:: XXREAL_3  semantic presentation begin  








definitionlet "x", "y" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )  ; redefine pred "x" :::"<="::: "y" means :: XXREAL_3:def 1 (Bool  "ex" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  "x") & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  "y") & (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "q")))  ")" )) if (Bool  "("  (Bool "x"  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  )) & (Bool "y"  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))  ")" )  otherwise (Bool  "("  (Bool "x"  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) "or" (Bool "y"  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ); end; 





:: deftheorem    defines :::"<="::: XXREAL_3:def 1 :  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  )) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y"))) "iff" (Bool  "ex" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Var "y"))) & (Bool (Set (Var "p"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "q")))  ")" ))  ")" )  ")"  &  "("  (Bool (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  )) "or"  "not" (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))  ")" )) "implies" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y"))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) "or" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" )  ")" )  ")"   ")" )); 
 registration
cluster   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v2_xxreal_0 :::"positive"::: )    ($#~v1_xreal_0  "non"   ($#v1_xreal_0 :::"real"::: )   )   for    ($#m1_hidden :::"set"::: )  ; 

cluster   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v3_xxreal_0 :::"negative"::: )    ($#~v1_xreal_0  "non"   ($#v1_xreal_0 :::"real"::: )   )   for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: XXREAL_3:1 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v2_xxreal_0 :::"positive"::: )    ($#~v1_xreal_0  "non"   ($#v1_xreal_0 :::"real"::: )   )    ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))) ; 
 
theorem :: XXREAL_3:2 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v3_xxreal_0 :::"negative"::: )    ($#~v1_xreal_0  "non"   ($#v1_xreal_0 :::"real"::: )   )    ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))) ; 
 registration
cluster   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )   ($#~v1_xreal_0  "non"   ($#v1_xreal_0 :::"real"::: )   )   ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v2_xxreal_0 :::"positive"::: )    for    ($#m1_hidden :::"set"::: )  ; 

cluster   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )   ($#~v1_xreal_0  "non"   ($#v1_xreal_0 :::"real"::: )   )   ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v3_xxreal_0 :::"negative"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: XXREAL_3:3 (Bool  "for" (Set (Var "x")) "," (Set (Var "z")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "z")))) "holds"  (Bool  "ex" (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "y"))) & (Bool (Set (Var "y"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "z")))  ")" ))) ; 
 begin  definitionlet "x", "y" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )  ; func "x" :::"+"::: "y" ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   means :: XXREAL_3:def 2 (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool "x"  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool "y"  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool it  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b"))))  ")" )) if (Bool  "("  (Bool "x" "is"   ($#v1_xreal_0 :::"real"::: )  ) & (Bool "y" "is"   ($#v1_xreal_0 :::"real"::: )  )  ")" ) (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) if (Bool  "("  (Bool  "("  (Bool "x"  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool "y"  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool "y"  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool "x"  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" )  ")" ) (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) if (Bool  "("  (Bool  "("  (Bool "x"  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool "y"  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool "y"  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool "x"  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" )  ")" )  otherwise (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )); commutativity  
(Bool  "for" (Set (Var "b1")) "," (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool  "("  (Bool (Bool (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  ) & (Bool (Set (Var "y")) "is"   ($#v1_xreal_0 :::"real"::: )  )) "implies" (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b"))))  ")" ))  ")"  &  "("  (Bool (Bool  "("  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" )  ")" )) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")"  &  "("  (Bool (Bool  "("  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" )  ")" )) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")"  & (Bool  "("  (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  ) & (Bool (Set (Var "y")) "is"   ($#v1_xreal_0 :::"real"::: )  )  ")" ) "or" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) "or" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "y")) "is"   ($#v1_xreal_0 :::"real"::: )  ) & (Bool (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  )) "implies" (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b"))))  ")" ))  ")"  &  "("  (Bool (Bool  "("  (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" )  ")" )) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")"  &  "("  (Bool (Bool  "("  (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" )  ")" )) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")"  & (Bool  "("  (Bool  "("  (Bool (Set (Var "y")) "is"   ($#v1_xreal_0 :::"real"::: )  ) & (Bool (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  )  ")" ) "or" (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) "or" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" ))
 ; end; 






:: deftheorem    defines :::"+"::: XXREAL_3:def 2 :  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "b3")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  ) & (Bool (Set (Var "y")) "is"   ($#v1_xreal_0 :::"real"::: )  )) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "y")))) "iff" (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b"))))  ")" ))  ")" )  ")"  &  "("  (Bool (Bool  "("  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" )  ")" )) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "y")))) "iff" (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" )  ")"  &  "("  (Bool (Bool  "("  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" )  ")" )) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "y")))) "iff" (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" )  ")"  & (Bool  "("  (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  ) & (Bool (Set (Var "y")) "is"   ($#v1_xreal_0 :::"real"::: )  )  ")" ) "or" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "y")))) "iff" (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")" )  ")" )); 
 definitionlet "x" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"-"::: "x" ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   means :: XXREAL_3:def 3 (Bool  "ex" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool "x"  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a"))))  ")" )) if (Bool "x" "is"   ($#v1_xreal_0 :::"real"::: )  ) (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) if (Bool "x"  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  otherwise (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )); involutiveness  
(Bool  "for" (Set (Var "b1")) "," (Set (Var "b2")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool  "("  (Bool (Bool (Set (Var "b2")) "is"   ($#v1_xreal_0 :::"real"::: )  )) "implies" (Bool  "ex" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a"))))  ")" ))  ")"  &  "("  (Bool (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b2")) "is"   ($#v1_xreal_0 :::"real"::: )  )) & (Bool (Bool  "not" (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )))) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "b1")) "is"   ($#v1_xreal_0 :::"real"::: )  )) "implies" (Bool  "ex" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a"))))  ")" ))  ")"  &  "("  (Bool (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))) "implies" (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b1")) "is"   ($#v1_xreal_0 :::"real"::: )  )) & (Bool (Bool  "not" (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )))) "implies" (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")"   ")" ))
 ; end; 





:: deftheorem    defines :::"-"::: XXREAL_3:def 3 :  (Bool  "for" (Set (Var "x")) "," (Set (Var "b2")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  )) "implies" (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_3 :::"-"::: )  (Set (Var "x")))) "iff" (Bool  "ex" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a"))))  ")" ))  ")" )  ")"  &  "("  (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_3 :::"-"::: )  (Set (Var "x")))) "iff" (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  )) & (Bool (Bool  "not" (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )))) "implies" (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_3 :::"-"::: )  (Set (Var "x")))) "iff" (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" )  ")"   ")" )); 
 definitionlet "x", "y" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )  ; func "x" :::"-"::: "y" ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   equals :: XXREAL_3:def 4 (Set "x"  ($#k1_xxreal_3 :::"+"::: )  (Set  "("  ($#k2_xxreal_3 :::"-"::: )  "y" ")" )); end; 






:: deftheorem    defines :::"-"::: XXREAL_3:def 4 :  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "x"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set  "("  ($#k2_xxreal_3 :::"-"::: )  (Set (Var "y")) ")" )))); 
 registrationlet "x", "y" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "a", "b" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; 
identify ; 
end; registrationlet "x" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "a" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; 
identify ; 
end; registrationlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k2_xxreal_3 :::"-"::: )  "r") ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v1_xreal_0 :::"real"::: )   ; 
end; registrationlet "r", "s" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "r"  ($#k1_xxreal_3 :::"+"::: )  "s") ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v1_xreal_0 :::"real"::: )   ; 

cluster (Set "r"  ($#k3_xxreal_3 :::"-"::: )  "s") ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v1_xreal_0 :::"real"::: )   ; 
end; registrationlet "x" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "y" be   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v1_xreal_0  "non"   ($#v1_xreal_0 :::"real"::: )   )    ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k1_xxreal_3 :::"+"::: )  "y") ->  ($#~v1_xreal_0  "non"   ($#v1_xreal_0 :::"real"::: )   )   for   ($#m1_hidden :::"number"::: )  ; 
end; registrationlet "x", "y" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v2_xxreal_0 :::"positive"::: )    ($#~v1_xreal_0  "non"   ($#v1_xreal_0 :::"real"::: )   )    ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k1_xxreal_3 :::"+"::: )  "y") ->   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v1_xreal_0  "non"   ($#v1_xreal_0 :::"real"::: )   )  ; 
end; registrationlet "x", "y" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v3_xxreal_0 :::"negative"::: )    ($#~v1_xreal_0  "non"   ($#v1_xreal_0 :::"real"::: )   )    ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k1_xxreal_3 :::"+"::: )  "y") ->   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v1_xreal_0  "non"   ($#v1_xreal_0 :::"real"::: )   )  ; 
end; registrationlet "x" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v3_xxreal_0 :::"negative"::: )    ($#~v1_xreal_0  "non"   ($#v1_xreal_0 :::"real"::: )   )    ($#m1_hidden :::"number"::: )  ; let "y" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v2_xxreal_0 :::"positive"::: )    ($#~v1_xreal_0  "non"   ($#v1_xreal_0 :::"real"::: )   )    ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k1_xxreal_3 :::"+"::: )  "y") ->   ($#v1_xboole_0 :::"zero"::: )     ($#v1_xxreal_0 :::"ext-real"::: )   ; 
end; registrationlet "x", "y" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "a", "b" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; 
identify ; 
end; 
theorem :: XXREAL_3:4 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "x")))) ; 
 
theorem :: XXREAL_3:5 (Bool (Set   ($#k2_xxreal_3 :::"-"::: )  (Set  ($#k2_xxreal_0 :::"-infty"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) ; 
 
theorem :: XXREAL_3:6 (Bool (Set   ($#k2_xxreal_3 :::"-"::: )  (Set  ($#k1_xxreal_0 :::"+infty"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) ; 
 
theorem :: XXREAL_3:7 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set  "("  ($#k2_xxreal_3 :::"-"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: XXREAL_3:8 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_3 :::"-"::: )  (Set (Var "y"))))) ; 
 
theorem :: XXREAL_3:9 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k2_xxreal_3 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_xxreal_3 :::"-"::: )  (Set (Var "x")) ")" )  ($#k1_xxreal_3 :::"+"::: )  (Set  "("  ($#k2_xxreal_3 :::"-"::: )  (Set (Var "y")) ")" )))) ; 
 




theorem :: XXREAL_3:10 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k2_xxreal_3 :::"-"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_3 :::"-"::: )  (Set (Var "g"))))) "holds"  (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "g")))) ; 
 
theorem :: XXREAL_3:11 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "r"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "g"))))) "holds"  (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "g"))))) ; 
 
theorem :: XXREAL_3:12 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "r"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "g"))))) "holds"  (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "g"))))) ; 
 
theorem :: XXREAL_3:13 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set  ($#k1_xxreal_0 :::"+infty"::: ) )  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Set (Var "x"))  ($#k3_xxreal_3 :::"-"::: )  (Set  ($#k1_xxreal_0 :::"+infty"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" )) ; 
 
theorem :: XXREAL_3:14 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set  ($#k2_xxreal_0 :::"-infty"::: ) )  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Set (Var "x"))  ($#k3_xxreal_3 :::"-"::: )  (Set  ($#k2_xxreal_0 :::"-infty"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" )) ; 
 
theorem :: XXREAL_3:15 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "x"))  ($#k3_xxreal_3 :::"-"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "x")))) ; 
 
theorem :: XXREAL_3:16 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "holds"  (Bool  "("   "not" (Bool (Set (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) "or" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" )) ; 
 
theorem :: XXREAL_3:17 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "holds"  (Bool  "("   "not" (Bool (Set (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) "or" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" )) ; 
 
theorem :: XXREAL_3:18 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "holds"  (Bool  "("   "not" (Bool (Set (Set (Var "x"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) "or" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" )) ; 
 
theorem :: XXREAL_3:19 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "holds"  (Bool  "("   "not" (Bool (Set (Set (Var "x"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) "or" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" )) ; 
 
theorem :: XXREAL_3:20 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "holds"  (Bool  "("  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) "or"  "not" (Bool (Set (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "y")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  )) "or" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  )) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))  ")" )  ")" )) ; 
 
theorem :: XXREAL_3:21 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "holds"  (Bool  "("  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" ) "or"  "not" (Bool (Set (Set (Var "x"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "y")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  )) "or" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  )) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))  ")" )  ")" )) ; 
 
theorem :: XXREAL_3:22 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  )) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "y"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "x")) ")" )  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "y"))) & (Bool (Set (Set  "(" (Set (Var "y"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "x")) ")" )  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "y")))  ")" )) ; 
 
theorem :: XXREAL_3:23 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))) "implies" (Bool (Set   ($#k2_xxreal_3 :::"-"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")"  &  "("  (Bool (Bool (Set   ($#k2_xxreal_3 :::"-"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))) "implies" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")"  &  "("  (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))) "implies" (Bool (Set   ($#k2_xxreal_3 :::"-"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")"  &  "("  (Bool (Bool (Set   ($#k2_xxreal_3 :::"-"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))) "implies" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")"   ")" )) ; 
 
theorem :: XXREAL_3:24 (Bool  "for" (Set (Var "z")) "," (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "z")) "is"   ($#v1_xreal_0 :::"real"::: )  )) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "z")) ")" )  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "z"))))) ; 
 
theorem :: XXREAL_3:25 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k2_xxreal_3 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_xxreal_3 :::"-"::: )  (Set (Var "y")) ")" )  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "x"))))) ; 
 
theorem :: XXREAL_3:26 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k2_xxreal_3 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_xxreal_3 :::"-"::: )  (Set (Var "x")) ")" )  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "y")))) & (Bool (Set   ($#k2_xxreal_3 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "x"))))  ")" )) ; 
 
theorem :: XXREAL_3:27 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k2_xxreal_3 :::"-"::: )  (Set  "(" (Set  "("  ($#k2_xxreal_3 :::"-"::: )  (Set (Var "x")) ")" )  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "y")))) & (Bool (Set   ($#k2_xxreal_3 :::"-"::: )  (Set  "(" (Set  "("  ($#k2_xxreal_3 :::"-"::: )  (Set (Var "x")) ")" )  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set  "("  ($#k2_xxreal_3 :::"-"::: )  (Set (Var "y")) ")" )))  ")" )) ; 
 
theorem :: XXREAL_3:28 (Bool  "for" (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y"))) & (Bool (Set (Var "y"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))) "holds"  (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "z"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "y")) ")" )  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "y"))))) ; 
 
theorem :: XXREAL_3:29 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) "or"  "not" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" ) & (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) "or"  "not" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) & (Bool  "not" (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" )) & (Bool  "not" (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" )) & (Bool  "not" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" )) & (Bool  "not" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ))) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "y")) ")" )  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "z")) ")" )))) ; 
 
theorem :: XXREAL_3:30 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) "or"  "not" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" ) & (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) "or"  "not" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) & (Bool  "("   "not" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) "or"  "not" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) & (Bool  "("   "not" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) "or"  "not" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" ) & (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) "or"  "not" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) & (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) "or"  "not" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" )) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "y")) ")" )  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "z")) ")" )))) ; 
 
theorem :: XXREAL_3:31 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) "or"  "not" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) & (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) "or"  "not" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" ) & (Bool  "("   "not" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) "or"  "not" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" ) & (Bool  "("   "not" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) "or"  "not" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) & (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) "or"  "not" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) & (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) "or"  "not" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" )) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "y")) ")" )  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k3_xxreal_3 :::"-"::: )  (Set  "(" (Set (Var "y"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "z")) ")" )))) ; 
 
theorem :: XXREAL_3:32 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) "or"  "not" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) & (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) "or"  "not" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" ) & (Bool  "("   "not" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) "or"  "not" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) & (Bool  "("   "not" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) "or"  "not" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" ) & (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) "or"  "not" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" ) & (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) "or"  "not" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" )) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "y")) ")" )  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k3_xxreal_3 :::"-"::: )  (Set  "(" (Set (Var "y"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "z")) ")" )))) ; 
 
theorem :: XXREAL_3:33 (Bool  "for" (Set (Var "z")) "," (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "z")) "is"   ($#v1_xreal_0 :::"real"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "z"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "x")) ")" )  ($#k3_xxreal_3 :::"-"::: )  (Set  "(" (Set (Var "z"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "y"))))) ; 
 
theorem :: XXREAL_3:34 (Bool  "for" (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "y")) "is"   ($#v1_xreal_0 :::"real"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "z"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "y")) ")" )  ($#k1_xxreal_3 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "z"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "x"))))) ; 
 begin  registrationlet "x", "y" be   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k1_xxreal_3 :::"+"::: )  "y") ->   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )  ; 
end; registrationlet "x", "y" be   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )    ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k1_xxreal_3 :::"+"::: )  "y") ->   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )  ; 
end; registrationlet "x" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#m1_hidden :::"number"::: )  ; let "y" be   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k1_xxreal_3 :::"+"::: )  "y") ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v2_xxreal_0 :::"positive"::: )   ; 

cluster (Set "y"  ($#k1_xxreal_3 :::"+"::: )  "x") ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v2_xxreal_0 :::"positive"::: )   ; 
end; registrationlet "x" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v3_xxreal_0 :::"negative"::: )     ($#m1_hidden :::"number"::: )  ; let "y" be   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )    ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k1_xxreal_3 :::"+"::: )  "y") ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v3_xxreal_0 :::"negative"::: )   ; 

cluster (Set "y"  ($#k1_xxreal_3 :::"+"::: )  "x") ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v3_xxreal_0 :::"negative"::: )   ; 
end; registrationlet "x" be   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )    ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k2_xxreal_3 :::"-"::: )  "x") ->   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )  ; 
end; registrationlet "x" be   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k2_xxreal_3 :::"-"::: )  "x") ->   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )  ; 
end; registrationlet "x" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k2_xxreal_3 :::"-"::: )  "x") ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v3_xxreal_0 :::"negative"::: )   ; 
end; registrationlet "x" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v3_xxreal_0 :::"negative"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k2_xxreal_3 :::"-"::: )  "x") ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v2_xxreal_0 :::"positive"::: )   ; 
end; registrationlet "x" be   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#m1_hidden :::"number"::: )  ; let "y" be   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )    ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k3_xxreal_3 :::"-"::: )  "y") ->   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )  ; 

cluster (Set "y"  ($#k3_xxreal_3 :::"-"::: )  "x") ->   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )  ; 
end; registrationlet "x" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#m1_hidden :::"number"::: )  ; let "y" be   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )    ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k3_xxreal_3 :::"-"::: )  "y") ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v2_xxreal_0 :::"positive"::: )   ; 

cluster (Set "y"  ($#k3_xxreal_3 :::"-"::: )  "x") ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v3_xxreal_0 :::"negative"::: )   ; 
end; registrationlet "x" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v3_xxreal_0 :::"negative"::: )     ($#m1_hidden :::"number"::: )  ; let "y" be   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k3_xxreal_3 :::"-"::: )  "y") ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v3_xxreal_0 :::"negative"::: )   ; 

cluster (Set "y"  ($#k3_xxreal_3 :::"-"::: )  "x") ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v2_xxreal_0 :::"positive"::: )   ; 
end; 
theorem :: XXREAL_3:35 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "z")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "y"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "z"))))) ; 
 
theorem :: XXREAL_3:36 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "w")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y"))) & (Bool (Set (Var "z"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "w")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "z")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "y"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "w"))))) ; 
 
theorem :: XXREAL_3:37 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "w")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y"))) & (Bool (Set (Var "z"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "w")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "w")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "y"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "z"))))) ; 
 
theorem :: XXREAL_3:38 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y"))) "iff" (Bool (Set   ($#k2_xxreal_3 :::"-"::: )  (Set (Var "y")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k2_xxreal_3 :::"-"::: )  (Set (Var "x"))))  ")" )) ; 
 
theorem :: XXREAL_3:39 (Bool  "for" (Set (Var "z")) "," (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "z")))) "holds"  (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "z"))))) ; 
 
theorem :: XXREAL_3:40 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y")))) "holds"  (Bool (Set (Set (Var "y"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: XXREAL_3:41 (Bool  "for" (Set (Var "z")) "," (Set (Var "y")) "," (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool  "("  (Bool (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))) "implies" (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"  &  "("  (Bool (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))) "implies" (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"  & (Bool (Set (Set (Var "x"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "y")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "z")))) "holds"  (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "z"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "y"))))) ; 
 
theorem :: XXREAL_3:42 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool  "("  (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))) "implies" (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "z")))  ")"  &  "("  (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))) "implies" (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "z")))  ")"  & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "z"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "y"))))) "holds"  (Bool (Set (Set (Var "x"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "y")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "z")))) ; 
 
theorem :: XXREAL_3:43 (Bool  "for" (Set (Var "z")) "," (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  )) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "y")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "z")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "y"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "z")))) & (Bool (Set (Set (Var "x"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "z")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "y"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "z"))))  ")" )) ; 
 
theorem :: XXREAL_3:44 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "x"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "z")))) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "y")) ")" )  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set  "(" (Set (Var "y"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "z")) ")" )))) ; 
 
theorem :: XXREAL_3:45 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  )) "holds"  (Bool  "("  (Bool (Set (Set (Var "y"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "z"))) "iff" (Bool (Set (Var "y"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "z"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "x"))))  ")" )) ; 
 
theorem :: XXREAL_3:46 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "x"))) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "y")))) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "y"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "x"))))) ; 
 
theorem :: XXREAL_3:47 (Bool  "for" (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "x"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "z"))) & (Bool (Set (Set (Var "z"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "y")))) "holds"  (Bool (Set (Var "z"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "y"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "x"))))) ; 
 
theorem :: XXREAL_3:48 (Bool  "for" (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "x"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "z"))) & (Bool (Set (Set (Var "z"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "y")))) "holds"  (Bool (Set (Var "z"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y")))) ; 
 
theorem :: XXREAL_3:49 (Bool  "for" (Set (Var "x")) "," (Set (Var "z")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "x"))) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "z")))) "holds"  (Bool  "ex" (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "y"))) & (Bool (Set (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "y")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "z")))  ")" ))) ; 
 
theorem :: XXREAL_3:50 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "x")))) "holds"  (Bool  "ex" (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "y"))) & (Bool (Set (Set (Var "y"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "y")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "x")))  ")" ))) ; 
 
theorem :: XXREAL_3:51 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "y"))) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set   ($#k2_xxreal_0 :::"-infty"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "y")))) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "y"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "x"))))) ; 
 
theorem :: XXREAL_3:52 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "holds"  (Bool  "("  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) "or"  "not" (Bool (Set (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "y")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "z"))) "or" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "z"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "z"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "y"))))  ")" )  ")" )) ; 
 
theorem :: XXREAL_3:53 (Bool  "for" (Set (Var "z")) "," (Set (Var "y")) "," (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "holds"  (Bool  "("  (Bool  "("  (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" ) "or"  "not" (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "z"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "y")))) "or" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "z"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "y")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "z")))  ")" )  ")" )) ; 
 
theorem :: XXREAL_3:54 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "holds"  (Bool  "("  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" ) "or"  "not" (Bool (Set (Set (Var "x"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "y")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "z"))) "or" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "z"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "z"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "y"))))  ")" )  ")" )) ; 
 
theorem :: XXREAL_3:55 (Bool  "for" (Set (Var "z")) "," (Set (Var "y")) "," (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "holds"  (Bool  "("  (Bool  "("  (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) "or"  "not" (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "z"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "y")))) "or" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "z"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Set (Var "x"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "y")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "z")))  ")" )  ")" )) ; 
 
theorem :: XXREAL_3:56 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "holds"  (Bool  "("  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" ) "or"  "not" (Bool (Set (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "y")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "z"))) "or" (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "z"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "y"))))  ")" )  ")" )) ; 
 
theorem :: XXREAL_3:57 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) "or"  "not" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" ) & (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) "or"  "not" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) & (Bool  "("   "not" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) "or"  "not" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "z"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "y"))))) "holds"  (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "y")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "z")))  ")" )) ; 
 
theorem :: XXREAL_3:58 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "holds"  (Bool  "("  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) "or"  "not" (Bool (Set (Set (Var "x"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "y")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "z"))) "or" (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" )) ; 
 
theorem :: XXREAL_3:59 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) "or"  "not" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" ) & (Bool  "("   "not" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) "or"  "not" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "z"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "y"))))) "holds"  (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))) ; 
 
theorem :: XXREAL_3:60 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k2_xxreal_3 :::"-"::: )  (Set (Var "y"))))) "implies" (Bool (Set (Var "y"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k2_xxreal_3 :::"-"::: )  (Set (Var "x"))))  ")"  &  "("  (Bool (Bool (Set   ($#k2_xxreal_3 :::"-"::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y")))) "implies" (Bool (Set   ($#k2_xxreal_3 :::"-"::: )  (Set (Var "y")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "x")))  ")"   ")" )) ; 
 
theorem :: XXREAL_3:61 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "e")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "e")))) "holds"  (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "y"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "e"))))  ")" )) "holds"  (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y")))) ; 
 



theorem :: XXREAL_3:62 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "t")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "t"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "t"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "y")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "t")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "y"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "t"))))) ; 
 
theorem :: XXREAL_3:63 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "t")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "t"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "t"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "y")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "t")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "y"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "t"))))) ; 
 
theorem :: XXREAL_3:64 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "w")) "," (Set (Var "z")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "y"))) & (Bool (Set (Var "w"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "z")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "w")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "y"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "z"))))) ; 
 
theorem :: XXREAL_3:65 (Bool  "for" (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "x"))) & (Bool (Set (Set (Var "z"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "x")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y")))) "holds"  (Bool (Set (Var "z"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y")))) ; 
 begin  definitionlet "x", "y" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )  ; func "x" :::"*"::: "y" ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   means :: XXREAL_3:def 5 (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool "x"  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool "y"  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool it  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b"))))  ")" )) if (Bool  "("  (Bool "x" "is"   ($#v1_xreal_0 :::"real"::: )  ) & (Bool "y" "is"   ($#v1_xreal_0 :::"real"::: )  )  ")" ) (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) if (Bool  "("  (Bool  "("   "not" (Bool "x" "is"   ($#v1_xreal_0 :::"real"::: )  ) "or"  "not" (Bool "y" "is"   ($#v1_xreal_0 :::"real"::: )  )  ")" ) & (Bool  "("  (Bool  "("  (Bool "x" "is"   ($#v2_xxreal_0 :::"positive"::: )  ) & (Bool "y" "is"   ($#v2_xxreal_0 :::"positive"::: )  )  ")" ) "or" (Bool  "("  (Bool "x" "is"   ($#v3_xxreal_0 :::"negative"::: )  ) & (Bool "y" "is"   ($#v3_xxreal_0 :::"negative"::: )  )  ")" )  ")" )  ")" ) (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) if (Bool  "("  (Bool  "("   "not" (Bool "x" "is"   ($#v1_xreal_0 :::"real"::: )  ) "or"  "not" (Bool "y" "is"   ($#v1_xreal_0 :::"real"::: )  )  ")" ) & (Bool  "("  (Bool  "("  (Bool "x" "is"   ($#v2_xxreal_0 :::"positive"::: )  ) & (Bool "y" "is"   ($#v3_xxreal_0 :::"negative"::: )  )  ")" ) "or" (Bool  "("  (Bool "x" "is"   ($#v3_xxreal_0 :::"negative"::: )  ) & (Bool "y" "is"   ($#v2_xxreal_0 :::"positive"::: )  )  ")" )  ")" )  ")" )  otherwise (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )); commutativity  
(Bool  "for" (Set (Var "b1")) "," (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool  "("  (Bool (Bool (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  ) & (Bool (Set (Var "y")) "is"   ($#v1_xreal_0 :::"real"::: )  )) "implies" (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b"))))  ")" ))  ")"  &  "("  (Bool (Bool  "("   "not" (Bool (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  ) "or"  "not" (Bool (Set (Var "y")) "is"   ($#v1_xreal_0 :::"real"::: )  )  ")" ) & (Bool  "("  (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v2_xxreal_0 :::"positive"::: )  ) & (Bool (Set (Var "y")) "is"   ($#v2_xxreal_0 :::"positive"::: )  )  ")" ) "or" (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v3_xxreal_0 :::"negative"::: )  ) & (Bool (Set (Var "y")) "is"   ($#v3_xxreal_0 :::"negative"::: )  )  ")" )  ")" )) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")"  &  "("  (Bool (Bool  "("   "not" (Bool (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  ) "or"  "not" (Bool (Set (Var "y")) "is"   ($#v1_xreal_0 :::"real"::: )  )  ")" ) & (Bool  "("  (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v2_xxreal_0 :::"positive"::: )  ) & (Bool (Set (Var "y")) "is"   ($#v3_xxreal_0 :::"negative"::: )  )  ")" ) "or" (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v3_xxreal_0 :::"negative"::: )  ) & (Bool (Set (Var "y")) "is"   ($#v2_xxreal_0 :::"positive"::: )  )  ")" )  ")" )) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")"  &  "("  (Bool (Bool  "("   "not" (Bool (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  ) "or"  "not" (Bool (Set (Var "y")) "is"   ($#v1_xreal_0 :::"real"::: )  )  ")" ) & (Bool  "("  (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  ) & (Bool (Set (Var "y")) "is"   ($#v1_xreal_0 :::"real"::: )  )  ")" ) "or" (Bool  "("  (Bool  "not" (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v2_xxreal_0 :::"positive"::: )  ) & (Bool (Set (Var "y")) "is"   ($#v2_xxreal_0 :::"positive"::: )  )  ")" )) & (Bool  "not" (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v3_xxreal_0 :::"negative"::: )  ) & (Bool (Set (Var "y")) "is"   ($#v3_xxreal_0 :::"negative"::: )  )  ")" ))  ")" )  ")" ) & (Bool  "("  (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  ) & (Bool (Set (Var "y")) "is"   ($#v1_xreal_0 :::"real"::: )  )  ")" ) "or" (Bool  "("  (Bool  "not" (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v2_xxreal_0 :::"positive"::: )  ) & (Bool (Set (Var "y")) "is"   ($#v3_xxreal_0 :::"negative"::: )  )  ")" )) & (Bool  "not" (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v3_xxreal_0 :::"negative"::: )  ) & (Bool (Set (Var "y")) "is"   ($#v2_xxreal_0 :::"positive"::: )  )  ")" ))  ")" )  ")" )) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "y")) "is"   ($#v1_xreal_0 :::"real"::: )  ) & (Bool (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  )) "implies" (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b"))))  ")" ))  ")"  &  "("  (Bool (Bool  "("   "not" (Bool (Set (Var "y")) "is"   ($#v1_xreal_0 :::"real"::: )  ) "or"  "not" (Bool (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  )  ")" ) & (Bool  "("  (Bool  "("  (Bool (Set (Var "y")) "is"   ($#v2_xxreal_0 :::"positive"::: )  ) & (Bool (Set (Var "x")) "is"   ($#v2_xxreal_0 :::"positive"::: )  )  ")" ) "or" (Bool  "("  (Bool (Set (Var "y")) "is"   ($#v3_xxreal_0 :::"negative"::: )  ) & (Bool (Set (Var "x")) "is"   ($#v3_xxreal_0 :::"negative"::: )  )  ")" )  ")" )) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")"  &  "("  (Bool (Bool  "("   "not" (Bool (Set (Var "y")) "is"   ($#v1_xreal_0 :::"real"::: )  ) "or"  "not" (Bool (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  )  ")" ) & (Bool  "("  (Bool  "("  (Bool (Set (Var "y")) "is"   ($#v2_xxreal_0 :::"positive"::: )  ) & (Bool (Set (Var "x")) "is"   ($#v3_xxreal_0 :::"negative"::: )  )  ")" ) "or" (Bool  "("  (Bool (Set (Var "y")) "is"   ($#v3_xxreal_0 :::"negative"::: )  ) & (Bool (Set (Var "x")) "is"   ($#v2_xxreal_0 :::"positive"::: )  )  ")" )  ")" )) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")"  &  "("  (Bool (Bool  "("   "not" (Bool (Set (Var "y")) "is"   ($#v1_xreal_0 :::"real"::: )  ) "or"  "not" (Bool (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  )  ")" ) & (Bool  "("  (Bool  "("  (Bool (Set (Var "y")) "is"   ($#v1_xreal_0 :::"real"::: )  ) & (Bool (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  )  ")" ) "or" (Bool  "("  (Bool  "not" (Bool  "("  (Bool (Set (Var "y")) "is"   ($#v2_xxreal_0 :::"positive"::: )  ) & (Bool (Set (Var "x")) "is"   ($#v2_xxreal_0 :::"positive"::: )  )  ")" )) & (Bool  "not" (Bool  "("  (Bool (Set (Var "y")) "is"   ($#v3_xxreal_0 :::"negative"::: )  ) & (Bool (Set (Var "x")) "is"   ($#v3_xxreal_0 :::"negative"::: )  )  ")" ))  ")" )  ")" ) & (Bool  "("  (Bool  "("  (Bool (Set (Var "y")) "is"   ($#v1_xreal_0 :::"real"::: )  ) & (Bool (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  )  ")" ) "or" (Bool  "("  (Bool  "not" (Bool  "("  (Bool (Set (Var "y")) "is"   ($#v2_xxreal_0 :::"positive"::: )  ) & (Bool (Set (Var "x")) "is"   ($#v3_xxreal_0 :::"negative"::: )  )  ")" )) & (Bool  "not" (Bool  "("  (Bool (Set (Var "y")) "is"   ($#v3_xxreal_0 :::"negative"::: )  ) & (Bool (Set (Var "x")) "is"   ($#v2_xxreal_0 :::"positive"::: )  )  ")" ))  ")" )  ")" )) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"   ")" ))
 ; end; 






:: deftheorem    defines :::"*"::: XXREAL_3:def 5 :  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "b3")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  ) & (Bool (Set (Var "y")) "is"   ($#v1_xreal_0 :::"real"::: )  )) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "y")))) "iff" (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b"))))  ")" ))  ")" )  ")"  &  "("  (Bool (Bool  "("   "not" (Bool (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  ) "or"  "not" (Bool (Set (Var "y")) "is"   ($#v1_xreal_0 :::"real"::: )  )  ")" ) & (Bool  "("  (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v2_xxreal_0 :::"positive"::: )  ) & (Bool (Set (Var "y")) "is"   ($#v2_xxreal_0 :::"positive"::: )  )  ")" ) "or" (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v3_xxreal_0 :::"negative"::: )  ) & (Bool (Set (Var "y")) "is"   ($#v3_xxreal_0 :::"negative"::: )  )  ")" )  ")" )) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "y")))) "iff" (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" )  ")"  &  "("  (Bool (Bool  "("   "not" (Bool (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  ) "or"  "not" (Bool (Set (Var "y")) "is"   ($#v1_xreal_0 :::"real"::: )  )  ")" ) & (Bool  "("  (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v2_xxreal_0 :::"positive"::: )  ) & (Bool (Set (Var "y")) "is"   ($#v3_xxreal_0 :::"negative"::: )  )  ")" ) "or" (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v3_xxreal_0 :::"negative"::: )  ) & (Bool (Set (Var "y")) "is"   ($#v2_xxreal_0 :::"positive"::: )  )  ")" )  ")" )) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "y")))) "iff" (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" )  ")"  &  "("  (Bool (Bool  "("   "not" (Bool (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  ) "or"  "not" (Bool (Set (Var "y")) "is"   ($#v1_xreal_0 :::"real"::: )  )  ")" ) & (Bool  "("  (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  ) & (Bool (Set (Var "y")) "is"   ($#v1_xreal_0 :::"real"::: )  )  ")" ) "or" (Bool  "("  (Bool  "not" (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v2_xxreal_0 :::"positive"::: )  ) & (Bool (Set (Var "y")) "is"   ($#v2_xxreal_0 :::"positive"::: )  )  ")" )) & (Bool  "not" (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v3_xxreal_0 :::"negative"::: )  ) & (Bool (Set (Var "y")) "is"   ($#v3_xxreal_0 :::"negative"::: )  )  ")" ))  ")" )  ")" ) & (Bool  "("  (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  ) & (Bool (Set (Var "y")) "is"   ($#v1_xreal_0 :::"real"::: )  )  ")" ) "or" (Bool  "("  (Bool  "not" (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v2_xxreal_0 :::"positive"::: )  ) & (Bool (Set (Var "y")) "is"   ($#v3_xxreal_0 :::"negative"::: )  )  ")" )) & (Bool  "not" (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v3_xxreal_0 :::"negative"::: )  ) & (Bool (Set (Var "y")) "is"   ($#v2_xxreal_0 :::"positive"::: )  )  ")" ))  ")" )  ")" )) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "y")))) "iff" (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")"   ")" )); 
 registrationlet "x", "y" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "a", "b" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; 
identify ; 
end; definitionlet "x" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )  ; func "x" :::""":::  ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   means :: XXREAL_3:def 6 (Bool  "ex" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool "x"  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool it  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k5_xcmplx_0 :::"""::: )  ))  ")" )) if (Bool "x" "is"   ($#v1_xreal_0 :::"real"::: )  )  otherwise (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )); end; 





:: deftheorem    defines :::"""::: XXREAL_3:def 6 :  (Bool  "for" (Set (Var "x")) "," (Set (Var "b2")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  )) "implies" (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_xxreal_3 :::"""::: )  )) "iff" (Bool  "ex" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k5_xcmplx_0 :::"""::: )  ))  ")" ))  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k5_xxreal_3 :::"""::: )  )) "iff" (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )  ")"   ")" )); 
 registrationlet "x" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "a" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; 
identify ; 
end; definitionlet "x", "y" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )  ; func "x" :::"/"::: "y" ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   equals :: XXREAL_3:def 7 (Set "x"  ($#k4_xxreal_3 :::"*"::: )  (Set  "(" "y"  ($#k5_xxreal_3 :::"""::: )  ")" )); end; 






:: deftheorem    defines :::"/"::: XXREAL_3:def 7 :  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "x"))  ($#k6_xxreal_3 :::"/"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set  "(" (Set (Var "y"))  ($#k5_xxreal_3 :::"""::: )  ")" )))); 
 registrationlet "x", "y" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "a", "b" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; 
identify ; 
end; registrationlet "x" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#m1_hidden :::"number"::: )  ; let "y" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v3_xxreal_0 :::"negative"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k4_xxreal_3 :::"*"::: )  "y") ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v3_xxreal_0 :::"negative"::: )   ; 
end; registrationlet "x", "y" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v3_xxreal_0 :::"negative"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k4_xxreal_3 :::"*"::: )  "y") ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v2_xxreal_0 :::"positive"::: )   ; 
end; registrationlet "x", "y" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v2_xxreal_0 :::"positive"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k4_xxreal_3 :::"*"::: )  "y") ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v2_xxreal_0 :::"positive"::: )   ; 
end; registrationlet "x" be   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )    ($#m1_hidden :::"number"::: )  ; let "y" be   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k4_xxreal_3 :::"*"::: )  "y") ->   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )  ; 
end; registrationlet "x", "y" be   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )    ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k4_xxreal_3 :::"*"::: )  "y") ->   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )  ; 
end; registrationlet "x", "y" be   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k4_xxreal_3 :::"*"::: )  "y") ->   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )  ; 
end; registrationlet "x" be   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )    ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k5_xxreal_3 :::"""::: )  ) ->   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )  ; 
end; registrationlet "x" be   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k5_xxreal_3 :::"""::: )  ) ->   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )  ; 
end; registrationlet "x" be   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#m1_hidden :::"number"::: )  ; let "y" be   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )    ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k6_xxreal_3 :::"/"::: )  "y") ->   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )  ; 

cluster (Set "y"  ($#k6_xxreal_3 :::"/"::: )  "x") ->   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )  ; 
end; registrationlet "x", "y" be   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k6_xxreal_3 :::"/"::: )  "y") ->   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )  ; 
end; registrationlet "x", "y" be   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )    ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k6_xxreal_3 :::"/"::: )  "y") ->   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )  ; 
end; registrationlet "x", "y" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )    ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k4_xxreal_3 :::"*"::: )  "y") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )    ($#v1_xxreal_0 :::"ext-real"::: )   ; 
end; registrationlet "x" be   ($#v1_xboole_0 :::"zero"::: )     ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )  ; let "y" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "x"  ($#k4_xxreal_3 :::"*"::: )  "y") ->   ($#v1_xboole_0 :::"zero"::: )     ($#v1_xxreal_0 :::"ext-real"::: )    for  ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )  ; 
end; 
theorem :: XXREAL_3:66 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set  "(" (Set (Var "y"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "y")) ")" )  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "z"))))) ; 
 registrationlet "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "r"  ($#k5_xxreal_3 :::"""::: )  ) ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v1_xreal_0 :::"real"::: )   ; 
end; registrationlet "r", "s" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "r"  ($#k4_xxreal_3 :::"*"::: )  "s") ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v1_xreal_0 :::"real"::: )   ; 

cluster (Set "r"  ($#k6_xxreal_3 :::"/"::: )  "s") ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v1_xreal_0 :::"real"::: )   ; 
end; registration
cluster (Set (Set  ($#k2_xxreal_0 :::"-infty"::: ) )  ($#k5_xxreal_3 :::"""::: )  ) ->   ($#v1_xboole_0 :::"zero"::: )     ($#v1_xxreal_0 :::"ext-real"::: )   ; 

cluster (Set (Set  ($#k1_xxreal_0 :::"+infty"::: ) )  ($#k5_xxreal_3 :::"""::: )  ) ->   ($#v1_xboole_0 :::"zero"::: )     ($#v1_xxreal_0 :::"ext-real"::: )   ; 
end; 
theorem :: XXREAL_3:67 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "g")) ")" )  ($#k5_xxreal_3 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k5_xxreal_3 :::"""::: )  ")" )  ($#k4_xxreal_3 :::"*"::: )  (Set  "(" (Set (Var "g"))  ($#k5_xxreal_3 :::"""::: )  ")" )))) ; 
 
theorem :: XXREAL_3:68 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "r"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "g"))))) "holds"  (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "g"))))) ; 
 
theorem :: XXREAL_3:69 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Bool  "not" (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )))) "holds"  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))) ; 
 
theorem :: XXREAL_3:70 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Bool  "not" (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )))) "holds"  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))) ; 
 
theorem :: XXREAL_3:71 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "z")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "z")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "y"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "z"))))) ; 
 
theorem :: XXREAL_3:72 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "y"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "z"))) & (Bool (Set (Var "z"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))) "holds"  (Bool (Set (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "z")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "y"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "z"))))) ; 
 
theorem :: XXREAL_3:73 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "holds"  (Bool  "("   "not" (Bool (Set (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "y")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  )) "or" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  )) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))  ")" ) "or" (Bool (Set (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: XXREAL_3:74 (Bool (Set (Set  ($#k1_xxreal_0 :::"+infty"::: ) )  ($#k5_xxreal_3 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) ; 
 
theorem :: XXREAL_3:75 (Bool (Set (Set  ($#k2_xxreal_0 :::"-infty"::: ) )  ($#k5_xxreal_3 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) ; 
 
theorem :: XXREAL_3:76 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "x"))  ($#k6_xxreal_3 :::"/"::: )  (Set  ($#k1_xxreal_0 :::"+infty"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: XXREAL_3:77 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "x"))  ($#k6_xxreal_3 :::"/"::: )  (Set  ($#k2_xxreal_0 :::"-infty"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: XXREAL_3:78 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "x"))  ($#k6_xxreal_3 :::"/"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: XXREAL_3:79 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "z")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k6_xxreal_3 :::"/"::: )  (Set (Var "z")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "y"))  ($#k6_xxreal_3 :::"/"::: )  (Set (Var "z"))))) ; 
 
theorem :: XXREAL_3:80 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "y"))) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "z"))) & (Bool (Set (Var "z"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))) "holds"  (Bool (Set (Set (Var "x"))  ($#k6_xxreal_3 :::"/"::: )  (Set (Var "z")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "y"))  ($#k6_xxreal_3 :::"/"::: )  (Set (Var "z"))))) ; 
 
theorem :: XXREAL_3:81 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Num 1)  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "x")))) ; 
 
theorem :: XXREAL_3:82 (Bool  "for" (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "holds"  (Bool  "("   "not" (Bool (Set (Set (Var "y"))  ($#k5_xxreal_3 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) "or" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) "or" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: XXREAL_3:83 (Bool  "for" (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "y"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))) "holds"  (Bool (Set (Set  ($#k1_xxreal_0 :::"+infty"::: ) )  ($#k6_xxreal_3 :::"/"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))) ; 
 
theorem :: XXREAL_3:84 (Bool  "for" (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "y"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k2_xxreal_0 :::"-infty"::: )  )  ($#r1_hidden :::"<>"::: )  (Set (Var "y")))) "holds"  (Bool (Set (Set  ($#k2_xxreal_0 :::"-infty"::: ) )  ($#k6_xxreal_3 :::"/"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))) ; 
 
theorem :: XXREAL_3:85 (Bool  "for" (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "y"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k2_xxreal_0 :::"-infty"::: )  )  ($#r1_hidden :::"<>"::: )  (Set (Var "y")))) "holds"  (Bool (Set (Set  ($#k1_xxreal_0 :::"+infty"::: ) )  ($#k6_xxreal_3 :::"/"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))) ; 
 
theorem :: XXREAL_3:86 (Bool  "for" (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "y"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))) "holds"  (Bool (Set (Set  ($#k2_xxreal_0 :::"-infty"::: ) )  ($#k6_xxreal_3 :::"/"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))) ; 
 
theorem :: XXREAL_3:87 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set  "(" (Num 1)  ($#k6_xxreal_3 :::"/"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Set  "(" (Num 1)  ($#k6_xxreal_3 :::"/"::: )  (Set (Var "x")) ")" )  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )) ; 
 
theorem :: XXREAL_3:88 (Bool  "for" (Set (Var "y")) "," (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k2_xxreal_0 :::"-infty"::: )  )  ($#r1_hidden :::"<>"::: )  (Set (Var "y"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "y")) ")" )  ($#k6_xxreal_3 :::"/"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set  "(" (Set (Var "y"))  ($#k6_xxreal_3 :::"/"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x")))  ")" )) ; 
 
theorem :: XXREAL_3:89 (Bool  "for" (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Set  ($#k1_xxreal_0 :::"+infty"::: ) )  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "y")))  ($#r1_hidden :::"<>"::: )  (Num 1)) & (Bool (Set (Set  ($#k2_xxreal_0 :::"-infty"::: ) )  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "y")))  ($#r1_hidden :::"<>"::: )  (Num 1))  ")" )) ; 
 
theorem :: XXREAL_3:90 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "y")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) & (Bool (Set (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "y")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) & (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  )))) "holds"  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))) ; 
 begin  
theorem :: XXREAL_3:91 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k2_xxreal_3 :::"-"::: )  (Num 1) ")" )  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_3 :::"-"::: )  (Set (Var "x"))))) ; 
 
theorem :: XXREAL_3:92 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k2_xxreal_3 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_xxreal_3 :::"-"::: )  (Set (Var "x")) ")" )  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "y"))))) ; 
 
theorem :: XXREAL_3:93 (Bool  "for" (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_3 :::"-"::: )  (Set (Var "z"))))) "holds"  (Bool (Set (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set  "(" (Set (Var "y"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "y")) ")" )  ($#k1_xxreal_3 :::"+"::: )  (Set  "(" (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "z")) ")" )))) ; 
 
theorem :: XXREAL_3:94 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Num 2)  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "x"))))) ; 
 
theorem :: XXREAL_3:95 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  )) "holds"  (Bool (Set (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set  "(" (Set (Var "y"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "y")) ")" )  ($#k1_xxreal_3 :::"+"::: )  (Set  "(" (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "z")) ")" )))) ; 
 
theorem :: XXREAL_3:96 (Bool  "for" (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "y"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "z"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set  "(" (Set (Var "y"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "y")) ")" )  ($#k1_xxreal_3 :::"+"::: )  (Set  "(" (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "z")) ")" )))) ; 
 
theorem :: XXREAL_3:97 (Bool  "for" (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "y"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "z"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set  "(" (Set (Var "y"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "y")) ")" )  ($#k1_xxreal_3 :::"+"::: )  (Set  "(" (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "z")) ")" )))) ; 
 
theorem :: XXREAL_3:98 (Bool  "for" (Set (Var "x")) "," (Set (Var "z")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set  "(" (Set  ($#k6_numbers :::"0"::: ) )  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k1_xxreal_3 :::"+"::: )  (Set  "(" (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "z")) ")" )))) ; 
 
theorem :: XXREAL_3:99 (Bool  "for" (Set (Var "f")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k2_xxreal_3 :::"-"::: )  (Set (Var "f")) ")" )  ($#k5_xxreal_3 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_3 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k5_xxreal_3 :::"""::: )  ")" )))) ; 
 
theorem :: XXREAL_3:100 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x")) "is"   ($#v1_xreal_0 :::"real"::: )  )) "holds"  (Bool (Set (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set  "(" (Set (Var "y"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "y")) ")" )  ($#k3_xxreal_3 :::"-"::: )  (Set  "(" (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "z")) ")" )))) ; 
 
theorem :: XXREAL_3:101 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y"))) & (Bool (Set (Var "z"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "y"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "z")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "z"))))) ; 
 
theorem :: XXREAL_3:102 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "y"))) & (Bool (Set (Var "z"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "z"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))) "holds"  (Bool (Set (Set (Var "y"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "z")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "x"))  ($#k4_xxreal_3 :::"*"::: )  (Set (Var "z"))))) ; 
 
theorem :: XXREAL_3:103 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y"))) & (Bool (Set (Var "z"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "y"))  ($#k6_xxreal_3 :::"/"::: )  (Set (Var "z")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "x"))  ($#k6_xxreal_3 :::"/"::: )  (Set (Var "z"))))) ; 
 
theorem :: XXREAL_3:104 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "y"))) & (Bool (Set (Var "z"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "z"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))) "holds"  (Bool (Set (Set (Var "y"))  ($#k6_xxreal_3 :::"/"::: )  (Set (Var "z")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Set (Var "x"))  ($#k6_xxreal_3 :::"/"::: )  (Set (Var "z"))))) ; 
 
theorem :: XXREAL_3:105 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k6_xxreal_3 :::"/"::: )  (Num 2) ")" )  ($#k1_xxreal_3 :::"+"::: )  (Set  "(" (Set (Var "x"))  ($#k6_xxreal_3 :::"/"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x")))) ;