:: EXTREAL2  semantic presentation begin  








begin  
theorem :: EXTREAL2:1 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"R_eal":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "a")))) "holds"  (Bool (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k18_complex1 :::"abs"::: )  (Set (Var "a")))))) ; 
 
theorem :: EXTREAL2:2 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"R_eal":::)  "holds"  (Bool  "("  (Bool (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set (Var "x"))) "or" (Bool (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k2_supinf_2 :::"-"::: )  (Set (Var "x"))))  ")" )) ; 
 
theorem :: EXTREAL2:3 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"R_eal":::) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) ))) ; 
 
theorem :: EXTREAL2:4 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"R_eal":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) ))) ; 
 
theorem :: EXTREAL2:5 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"R_eal":::) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: EXTREAL2:6 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"R_eal":::)  "st" (Bool (Bool (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k2_supinf_2 :::"-"::: )  (Set (Var "x")))) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: EXTREAL2:7 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"R_eal":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k2_supinf_2 :::"-"::: )  (Set (Var "x"))))) ; 
 
theorem :: EXTREAL2:8 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"R_eal":::) "holds"  (Bool (Set  ($#k3_extreal1 :::"|."::: ) (Set  "(" (Set (Var "x"))  ($#k1_extreal1 :::"*"::: )  (Set (Var "y")) ")" ) ($#k3_extreal1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) )  ($#k1_extreal1 :::"*"::: )  (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "y")) ($#k3_extreal1 :::".|"::: ) )))) ; 
 
theorem :: EXTREAL2:9 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"R_eal":::) "holds"   (Bool  "("  (Bool (Set   ($#k2_supinf_2 :::"-"::: )  (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "x"))) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) ))  ")" )) ; 
 
theorem :: EXTREAL2:10 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"R_eal":::)  "st" (Bool (Bool (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "y")))) "holds"  (Bool  "("  (Bool (Set   ($#k2_supinf_2 :::"-"::: )  (Set (Var "y")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "x"))) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "y")))  ")" )) ; 
 
theorem :: EXTREAL2:11 (Bool  "for" (Set (Var "y")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"R_eal":::)  "st" (Bool (Bool (Set   ($#k2_supinf_2 :::"-"::: )  (Set (Var "y")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "x"))) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "y")))) "holds"  (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "y"))) & (Bool (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "y")))  ")" )) ; 
 
theorem :: EXTREAL2:12 (Bool  "for" (Set (Var "y")) "," (Set (Var "x")) "being"   ($#m1_subset_1 :::"R_eal":::) "holds"   (Bool  "("  (Bool  "("  (Bool (Set   ($#k2_supinf_2 :::"-"::: )  (Set (Var "y")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "x"))) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y")))  ")" ) "iff" (Bool (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y")))  ")" )) ; 
 
theorem :: EXTREAL2:13 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"R_eal":::) "holds"  (Bool (Set  ($#k3_extreal1 :::"|."::: ) (Set  "(" (Set (Var "x"))  ($#k3_supinf_2 :::"+"::: )  (Set (Var "y")) ")" ) ($#k3_extreal1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) )  ($#k3_supinf_2 :::"+"::: )  (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "y")) ($#k3_extreal1 :::".|"::: ) )))) ; 
 
theorem :: EXTREAL2:14 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"R_eal":::)  "st" (Bool (Bool (Set   ($#k2_supinf_1 :::"-infty"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "x"))) & (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_supinf_1 :::"+infty"::: )  )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) )  ($#k1_extreal1 :::"*"::: )  (Set  ($#k3_extreal1 :::"|."::: ) (Set  "(" (Set  ($#k8_mesfunc1 :::"1."::: ) )  ($#k2_extreal1 :::"/"::: )  (Set (Var "x")) ")" ) ($#k3_extreal1 :::".|"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k8_mesfunc1 :::"1."::: )  ))) ; 
 
theorem :: EXTREAL2:15 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"R_eal":::)  "st" (Bool (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_supinf_1 :::"+infty"::: )  )) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_supinf_1 :::"-infty"::: )  ))  ")" )) "holds"  (Bool (Set (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) )  ($#k1_extreal1 :::"*"::: )  (Set  ($#k3_extreal1 :::"|."::: ) (Set  "(" (Set  ($#k8_mesfunc1 :::"1."::: ) )  ($#k2_extreal1 :::"/"::: )  (Set (Var "x")) ")" ) ($#k3_extreal1 :::".|"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: EXTREAL2:16 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"R_eal":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set  ($#k3_extreal1 :::"|."::: ) (Set  "(" (Set  ($#k8_mesfunc1 :::"1."::: ) )  ($#k2_extreal1 :::"/"::: )  (Set (Var "x")) ")" ) ($#k3_extreal1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k8_mesfunc1 :::"1."::: ) )  ($#k2_extreal1 :::"/"::: )  (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) )))) ; 
 
theorem :: EXTREAL2:17 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"R_eal":::)  "st" (Bool (Bool  "("  (Bool  "("  (Bool (Bool  "not" (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_supinf_1 :::"-infty"::: )  ))) & (Bool (Bool  "not" (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_supinf_1 :::"+infty"::: )  )))  ")" ) "or" (Bool  "("  (Bool (Bool  "not" (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_supinf_1 :::"-infty"::: )  ))) & (Bool (Bool  "not" (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_supinf_1 :::"+infty"::: )  )))  ")" )  ")" ) & (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set  ($#k3_extreal1 :::"|."::: ) (Set  "(" (Set (Var "x"))  ($#k2_extreal1 :::"/"::: )  (Set (Var "y")) ")" ) ($#k3_extreal1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) )  ($#k2_extreal1 :::"/"::: )  (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "y")) ($#k3_extreal1 :::".|"::: ) )))) ; 
 
theorem :: EXTREAL2:18 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"R_eal":::) "holds"  (Bool (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k3_extreal1 :::"|."::: ) (Set  "("  ($#k2_supinf_2 :::"-"::: )  (Set (Var "x")) ")" ) ($#k3_extreal1 :::".|"::: ) ))) ; 
 
theorem :: EXTREAL2:19 (Bool  "("  (Bool (Set  ($#k3_extreal1 :::"|."::: ) (Set  ($#k1_supinf_1 :::"+infty"::: ) ) ($#k3_extreal1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k1_supinf_1 :::"+infty"::: )  )) & (Bool (Set  ($#k3_extreal1 :::"|."::: ) (Set  ($#k2_supinf_1 :::"-infty"::: ) ) ($#k3_extreal1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k1_supinf_1 :::"+infty"::: )  ))  ")" ) ; 
 
theorem :: EXTREAL2:20 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"R_eal":::)  "st" (Bool (Bool  "("  (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Real":::)) "or" (Bool (Set (Var "y")) "is"   ($#m1_subset_1 :::"Real":::))  ")" )) "holds"  (Bool (Set (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) )  ($#k4_supinf_2 :::"-"::: )  (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "y")) ($#k3_extreal1 :::".|"::: ) ))  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k3_extreal1 :::"|."::: ) (Set  "(" (Set (Var "x"))  ($#k4_supinf_2 :::"-"::: )  (Set (Var "y")) ")" ) ($#k3_extreal1 :::".|"::: ) ))) ; 
 
theorem :: EXTREAL2:21 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"R_eal":::) "holds"  (Bool (Set  ($#k3_extreal1 :::"|."::: ) (Set  "(" (Set (Var "x"))  ($#k4_supinf_2 :::"-"::: )  (Set (Var "y")) ")" ) ($#k3_extreal1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) )  ($#k3_supinf_2 :::"+"::: )  (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "y")) ($#k3_extreal1 :::".|"::: ) )))) ; 
 
theorem :: EXTREAL2:22 canceled; 
 
theorem :: EXTREAL2:23 (Bool  "for" (Set (Var "x")) "," (Set (Var "z")) "," (Set (Var "y")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"R_eal":::)  "st" (Bool (Bool (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "z"))) & (Bool (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "y")) ($#k3_extreal1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "w")))) "holds"  (Bool (Set  ($#k3_extreal1 :::"|."::: ) (Set  "(" (Set (Var "x"))  ($#k3_supinf_2 :::"+"::: )  (Set (Var "y")) ")" ) ($#k3_extreal1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "z"))  ($#k3_supinf_2 :::"+"::: )  (Set (Var "w"))))) ; 
 
theorem :: EXTREAL2:24 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"R_eal":::)  "st" (Bool (Bool  "("  (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Real":::)) "or" (Bool (Set (Var "y")) "is"   ($#m1_subset_1 :::"Real":::))  ")" )) "holds"  (Bool (Set  ($#k3_extreal1 :::"|."::: ) (Set  "(" (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) )  ($#k4_supinf_2 :::"-"::: )  (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "y")) ($#k3_extreal1 :::".|"::: ) ) ")" ) ($#k3_extreal1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<="::: )  (Set  ($#k3_extreal1 :::"|."::: ) (Set  "(" (Set (Var "x"))  ($#k4_supinf_2 :::"-"::: )  (Set (Var "y")) ")" ) ($#k3_extreal1 :::".|"::: ) ))) ; 
 
theorem :: EXTREAL2:25 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"R_eal":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "x"))  ($#k1_extreal1 :::"*"::: )  (Set (Var "y"))))) "holds"  (Bool (Set  ($#k3_extreal1 :::"|."::: ) (Set  "(" (Set (Var "x"))  ($#k3_supinf_2 :::"+"::: )  (Set (Var "y")) ")" ) ($#k3_extreal1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) )  ($#k3_supinf_2 :::"+"::: )  (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "y")) ($#k3_extreal1 :::".|"::: ) )))) ; 
 begin  
theorem :: EXTREAL2:26 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"R_eal":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_supinf_1 :::"+infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_supinf_1 :::"+infty"::: )  )) & (Bool  "not" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_supinf_1 :::"+infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_supinf_1 :::"+infty"::: )  ))  ")" )) & (Bool  "not" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_supinf_1 :::"-infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_supinf_1 :::"-infty"::: )  ))  ")" ))) "holds"  (Bool (Set   ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "x"))  ($#k3_supinf_2 :::"+"::: )  (Set (Var "y")) ")" )  ($#k4_supinf_2 :::"-"::: )  (Set  ($#k3_extreal1 :::"|."::: ) (Set  "(" (Set (Var "x"))  ($#k4_supinf_2 :::"-"::: )  (Set (Var "y")) ")" ) ($#k3_extreal1 :::".|"::: ) ) ")" )  ($#k2_extreal1 :::"/"::: )  (Set  "("  ($#k1_measure6 :::"R_EAL"::: )  (Num 2) ")" )))) ; 
 
theorem :: EXTREAL2:27 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"R_eal":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_supinf_1 :::"-infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_supinf_1 :::"-infty"::: )  )) & (Bool  "not" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_supinf_1 :::"+infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_supinf_1 :::"+infty"::: )  ))  ")" )) & (Bool  "not" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_supinf_1 :::"-infty"::: )  )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_supinf_1 :::"-infty"::: )  ))  ")" ))) "holds"  (Bool (Set   ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "x"))  ($#k3_supinf_2 :::"+"::: )  (Set (Var "y")) ")" )  ($#k3_supinf_2 :::"+"::: )  (Set  ($#k3_extreal1 :::"|."::: ) (Set  "(" (Set (Var "x"))  ($#k4_supinf_2 :::"-"::: )  (Set (Var "y")) ")" ) ($#k3_extreal1 :::".|"::: ) ) ")" )  ($#k2_extreal1 :::"/"::: )  (Set  "("  ($#k1_measure6 :::"R_EAL"::: )  (Num 2) ")" )))) ; 
 definitionlet "x", "y" be   ($#m1_subset_1 :::"R_eal":::); :: original: :::"max"::: redefine func  :::"max":::  "(" "x" "," "y" ")"  ->   ($#m1_subset_1 :::"R_eal":::); :: original: :::"min"::: redefine func  :::"min":::  "(" "x" "," "y" ")"  ->   ($#m1_subset_1 :::"R_eal":::); end; 
theorem :: EXTREAL2:28 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"R_eal":::) "holds"  (Bool (Set (Set  "("  ($#k2_extreal2 :::"min"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" )  ($#k3_supinf_2 :::"+"::: )  (Set  "("  ($#k1_extreal2 :::"max"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k3_supinf_2 :::"+"::: )  (Set (Var "y"))))) ; 
 begin  
theorem :: EXTREAL2:29 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"R_eal":::)  "holds"  (Bool  "("   "not" (Bool (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k1_supinf_1 :::"+infty"::: )  )) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_supinf_1 :::"+infty"::: )  )) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_supinf_1 :::"-infty"::: )  ))  ")" )) ; 
 
theorem :: EXTREAL2:30 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"R_eal":::) "holds"   (Bool  "("  (Bool (Set  ($#k3_extreal1 :::"|."::: ) (Set (Var "x")) ($#k3_extreal1 :::".|"::: ) )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_supinf_1 :::"+infty"::: )  )) "iff" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))  ")" )) ;