:: XXREAL_0  semantic presentation begin  


definitionlet "x" be    ($#m1_hidden :::"set"::: )  ; attr "x" is  :::"ext-real":::  means :: XXREAL_0:def 1 (Bool "x"  ($#r2_hidden :::"in"::: )  (Set   ($#k7_numbers :::"ExtREAL"::: )  )); end; 




:: deftheorem    defines :::"ext-real"::: XXREAL_0:def 1 :  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x")) "is"   ($#v1_xxreal_0 :::"ext-real"::: )  ) "iff" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k7_numbers :::"ExtREAL"::: )  ))  ")" )); 
 registration
cluster   ($#v1_xxreal_0 :::"ext-real"::: )    for    ($#m1_hidden :::"set"::: )  ; 

cluster   ->   ($#v1_xxreal_0 :::"ext-real"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k7_numbers :::"ExtREAL"::: )  ); 
end; registration


  ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )  


(Bool  "ex" (Set (Var "b1")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "for" (Set (Var "b2")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set (Var "b1")))))
 
; 
end; definitionfunc  :::"+infty":::  ->    ($#m1_hidden :::"set"::: )   equals :: XXREAL_0:def 2 (Set   ($#k1_numbers :::"REAL"::: )  ); func  :::"-infty":::  ->    ($#m1_hidden :::"set"::: )   equals :: XXREAL_0:def 3 (Set  ($#k4_tarski :::"["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) ($#k4_tarski :::"]"::: ) ); end; 








:: deftheorem    defines :::"+infty"::: XXREAL_0:def 2 :  (Bool (Set   ($#k1_xxreal_0 :::"+infty"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k1_numbers :::"REAL"::: )  )); 
 
:: deftheorem    defines :::"-infty"::: XXREAL_0:def 3 :  (Bool (Set   ($#k2_xxreal_0 :::"-infty"::: )  )  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k1_numbers :::"REAL"::: ) ) ($#k4_tarski :::"]"::: ) )); 
 definitionredefine func  :::"ExtREAL":::  equals :: XXREAL_0:def 4 (Set (Set  ($#k1_numbers :::"REAL"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k1_xxreal_0 :::"+infty"::: ) ) "," (Set  ($#k2_xxreal_0 :::"-infty"::: ) ) ($#k2_tarski :::"}"::: ) )); end; 




:: deftheorem    defines :::"ExtREAL"::: XXREAL_0:def 4 :  (Bool (Set   ($#k7_numbers :::"ExtREAL"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k1_numbers :::"REAL"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k1_xxreal_0 :::"+infty"::: ) ) "," (Set  ($#k2_xxreal_0 :::"-infty"::: ) ) ($#k2_tarski :::"}"::: ) ))); 
 registration
cluster (Set   ($#k1_xxreal_0 :::"+infty"::: )  ) ->   ($#v1_xxreal_0 :::"ext-real"::: )   ; 

cluster (Set   ($#k2_xxreal_0 :::"-infty"::: )  ) ->   ($#v1_xxreal_0 :::"ext-real"::: )   ; 
end; definitionlet "x", "y" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )  ; pred "x" :::"<="::: "y" means :: XXREAL_0:def 5 (Bool  "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  ) "st"  (Bool  "("  (Bool "x"  ($#r1_hidden :::"="::: )  (Set (Var "x9"))) & (Bool "y"  ($#r1_hidden :::"="::: )  (Set (Var "y9"))) & (Bool (Set (Var "x9"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "y9")))  ")" )) if (Bool  "("  (Bool "x"  ($#r2_hidden :::"in"::: )  (Set   ($#k2_arytm_2 :::"REAL+"::: )  )) & (Bool "y"  ($#r2_hidden :::"in"::: )  (Set   ($#k2_arytm_2 :::"REAL+"::: )  ))  ")" ) (Bool  "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  ) "st"  (Bool  "("  (Bool "x"  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x9")) ($#k4_tarski :::"]"::: ) )) & (Bool "y"  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "y9"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "x9")))  ")" )) if (Bool  "("  (Bool "x"  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool "y"  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))  ")" )  otherwise (Bool  "("  (Bool  "("  (Bool "y"  ($#r2_hidden :::"in"::: )  (Set   ($#k2_arytm_2 :::"REAL+"::: )  )) & (Bool "x"  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))  ")" ) "or" (Bool "x"  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) "or" (Bool "y"  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" ); reflexivity  
(Bool  "for" (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_arytm_2 :::"REAL+"::: )  )) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_arytm_2 :::"REAL+"::: )  ))) "implies" (Bool  "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "x9"))) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y9"))) & (Bool (Set (Var "x9"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "y9")))  ")" ))  ")"  &  "("  (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) "implies" (Bool  "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "y9"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "x9")))  ")" ))  ")"  &  "("  (Bool (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_arytm_2 :::"REAL+"::: )  )) "or"  "not" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_arytm_2 :::"REAL+"::: )  ))  ")" ) & (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) "or"  "not" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))  ")" ) & (Bool  "not" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_arytm_2 :::"REAL+"::: )  )) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))  ")" )) & (Bool (Bool  "not" (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )))) "implies" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")"   ")" ))
 ; connectedness  
(Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_arytm_2 :::"REAL+"::: )  )) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_arytm_2 :::"REAL+"::: )  )) & (Bool  "("   "for" (Set (Var "x9")) "," (Set (Var "y9")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  )  "holds"  (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "x9"))) "or"  "not" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "y9"))) "or"  "not" (Bool (Set (Var "x9"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "y9")))  ")" )  ")" )  ")" ) "or" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool  "("   "for" (Set (Var "x9")) "," (Set (Var "y9")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  )  "holds"  (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x9")) ($#k4_tarski :::"]"::: ) )) "or"  "not" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) )) "or"  "not" (Bool (Set (Var "y9"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "x9")))  ")" )  ")" )  ")" ) "or" (Bool  "("  (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_arytm_2 :::"REAL+"::: )  )) "or"  "not" (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_arytm_2 :::"REAL+"::: )  ))  ")" ) & (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) "or"  "not" (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))  ")" ) & (Bool  "not" (Bool  "("  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_arytm_2 :::"REAL+"::: )  )) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))  ")" )) & (Bool (Bool  "not" (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))) & (Bool (Bool  "not" (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )))  ")" )  ")" )) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_arytm_2 :::"REAL+"::: )  )) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_arytm_2 :::"REAL+"::: )  ))) "implies" (Bool  "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "x9"))) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y9"))) & (Bool (Set (Var "x9"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "y9")))  ")" ))  ")"  &  "("  (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) "implies" (Bool  "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "y9"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "x9")))  ")" ))  ")"  &  "("  (Bool (Bool  "("   "not" (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_arytm_2 :::"REAL+"::: )  )) "or"  "not" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_arytm_2 :::"REAL+"::: )  ))  ")" ) & (Bool  "("   "not" (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) "or"  "not" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))  ")" ) & (Bool  "not" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_arytm_2 :::"REAL+"::: )  )) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))  ")" )) & (Bool (Bool  "not" (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )))) "implies" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")"   ")" ))
 ; end; 





:: deftheorem    defines :::"<="::: XXREAL_0:def 5 :  (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   ($#k2_arytm_2 :::"REAL+"::: )  )) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_arytm_2 :::"REAL+"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y"))) "iff" (Bool  "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "x9"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "y9"))) & (Bool (Set (Var "x9"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "y9")))  ")" ))  ")" )  ")"  &  "("  (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) "implies" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y"))) "iff" (Bool  "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k2_arytm_2 :::"REAL+"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "y9"))  ($#r1_arytm_2 :::"<='"::: )  (Set (Var "x9")))  ")" ))  ")" )  ")"  &  "("  (Bool (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_arytm_2 :::"REAL+"::: )  )) "or"  "not" (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_arytm_2 :::"REAL+"::: )  ))  ")" ) & (Bool  "("   "not" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) "or"  "not" (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))  ")" )) "implies" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "y"))) "iff" (Bool  "("  (Bool  "("  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_arytm_2 :::"REAL+"::: )  )) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k2_arytm_2 :::"REAL+"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))  ")" ) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  )) "or" (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" )  ")" )  ")"   ")" )); 
 





notationlet "a", "b" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )  ; synonym "b" :::">="::: "a" for "a" :::"<="::: "b"; antonym "b" :::"<"::: "a" for "a" :::"<="::: "b"; antonym "a" :::">"::: "b" for "a" :::"<="::: "b"; end; 
theorem :: XXREAL_0:1 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a")))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))) ; 
 
theorem :: XXREAL_0:2 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "c")))) "holds"  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "c")))) ; 
 
theorem :: XXREAL_0:3 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))) ; 
 
theorem :: XXREAL_0:4 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k1_xxreal_0 :::"+infty"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a")))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))) ; 
 
theorem :: XXREAL_0:5 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))) ; 
 
theorem :: XXREAL_0:6 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k2_xxreal_0 :::"-infty"::: )  )  ($#r1_xxreal_0 :::">="::: )  (Set (Var "a")))) "holds"  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))) ; 
 
theorem :: XXREAL_0:7 (Bool (Set   ($#k2_xxreal_0 :::"-infty"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) ; 
 
theorem :: XXREAL_0:8 (Bool (Bool  "not" (Set   ($#k1_xxreal_0 :::"+infty"::: )  )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))) ; 
 
theorem :: XXREAL_0:9 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))) "holds"  (Bool (Set   ($#k1_xxreal_0 :::"+infty"::: )  )  ($#r1_xxreal_0 :::">"::: )  (Set (Var "a")))) ; 
 
theorem :: XXREAL_0:10 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  )) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "a"))) & (Bool (Bool  "not" (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  )))) "holds"  (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))) ; 
 
theorem :: XXREAL_0:11 (Bool (Bool  "not" (Set   ($#k2_xxreal_0 :::"-infty"::: )  )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))) ; 
 
theorem :: XXREAL_0:12 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))) "holds"  (Bool (Set   ($#k2_xxreal_0 :::"-infty"::: )  )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a")))) ; 
 
theorem :: XXREAL_0:13 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  )) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Bool  "not" (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  )))) "holds"  (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))) ; 
 
theorem :: XXREAL_0:14 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  )) "or" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )) "or" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))  ")" )) ; 
 begin  registration
cluster   ($#v7_ordinal1 :::"natural"::: )    ->   ($#v1_xxreal_0 :::"ext-real"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; notationlet "a" be    ($#m1_hidden :::"number"::: )  ; synonym  :::"zero"::: "a" for  :::"empty"::: ; end; definitionlet "a" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )  ; attr "a" is  :::"positive":::  means :: XXREAL_0:def 6 (Bool "a"  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )); attr "a" is  :::"negative":::  means :: XXREAL_0:def 7 (Bool "a"  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )); redefine attr "a" is  :::"empty":::  means :: XXREAL_0:def 8 (Bool "a"  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )); end; 












:: deftheorem    defines :::"positive"::: XXREAL_0:def 6 :  (Bool  "for" (Set (Var "a")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "a")) "is"   ($#v2_xxreal_0 :::"positive"::: )  ) "iff" (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )); 
 
:: deftheorem    defines :::"negative"::: XXREAL_0:def 7 :  (Bool  "for" (Set (Var "a")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "a")) "is"   ($#v3_xxreal_0 :::"negative"::: )  ) "iff" (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )); 
 
:: deftheorem    defines :::"zero"::: XXREAL_0:def 8 :  (Bool  "for" (Set (Var "a")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "a")) "is"   ($#v1_xboole_0 :::"zero"::: )  ) "iff" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )); 
 registration
cluster   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v2_xxreal_0 :::"positive"::: )    ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )    ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )   for    ($#m1_hidden :::"set"::: )  ; 

cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )    ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )   ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v2_xxreal_0 :::"positive"::: )    for    ($#m1_hidden :::"set"::: )  ; 

cluster   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v3_xxreal_0 :::"negative"::: )    ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )    ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )   for    ($#m1_hidden :::"set"::: )  ; 

cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )    ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )   ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v3_xxreal_0 :::"negative"::: )    for    ($#m1_hidden :::"set"::: )  ; 

cluster   ($#v1_xboole_0 :::"zero"::: )     ($#v1_xxreal_0 :::"ext-real"::: )    ->   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )   ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )   for    ($#m1_hidden :::"set"::: )  ; 

cluster   ($#v1_xxreal_0 :::"ext-real"::: )    ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )   ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )   ->   ($#v1_xboole_0 :::"zero"::: )     ($#v1_xxreal_0 :::"ext-real"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registration
cluster (Set   ($#k1_xxreal_0 :::"+infty"::: )  ) ->   ($#v2_xxreal_0 :::"positive"::: )   ; 

cluster (Set   ($#k2_xxreal_0 :::"-infty"::: )  ) ->   ($#v3_xxreal_0 :::"negative"::: )   ; 
end; registration
cluster   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v2_xxreal_0 :::"positive"::: )    for    ($#m1_hidden :::"set"::: )  ; 

cluster   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v3_xxreal_0 :::"negative"::: )    for    ($#m1_hidden :::"set"::: )  ; 

cluster   ($#v1_xboole_0 :::"zero"::: )     ($#v1_xxreal_0 :::"ext-real"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; begin  definitionlet "a", "b" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"min":::  "(" "a" "," "b" ")"  ->    ($#m1_hidden :::"set"::: )   equals :: XXREAL_0:def 9 "a" if (Bool "a"  ($#r1_xxreal_0 :::"<="::: )  "b")  otherwise "b"; commutativity  
(Bool  "for" (Set (Var "b1")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool  "("  (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))))) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" ) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a")))) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))))) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")"   ")" )))
 ; idempotence  
(Bool  "for" (Set (Var "a")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a")))) "implies" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))))) "implies" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")"   ")" ))
 ; func  :::"max":::  "(" "a" "," "b" ")"  ->    ($#m1_hidden :::"set"::: )   equals :: XXREAL_0:def 10 "a" if (Bool "b"  ($#r1_xxreal_0 :::"<="::: )  "a")  otherwise "b"; commutativity  
(Bool  "for" (Set (Var "b1")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool  "("  (Bool (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a")))) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))))) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" ) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))))) "implies" (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")"   ")" )))
 ; idempotence  
(Bool  "for" (Set (Var "a")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a")))) "implies" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))))) "implies" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")"   ")" ))
 ; end; 












:: deftheorem    defines :::"min"::: XXREAL_0:def 9 :  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) "implies" (Bool (Set   ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))))) "implies" (Bool (Set   ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")"   ")" )); 
 
:: deftheorem    defines :::"max"::: XXREAL_0:def 10 :  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a")))) "implies" (Bool (Set   ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))))) "implies" (Bool (Set   ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")"   ")" )); 
 
theorem :: XXREAL_0:15 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "holds"  (Bool  "("  (Bool (Set   ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "a"))) "or" (Bool (Set   ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" )) ; 
 
theorem :: XXREAL_0:16 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "holds"  (Bool  "("  (Bool (Set   ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "a"))) "or" (Bool (Set   ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" )) ; 
 registrationlet "a", "b" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k3_xxreal_0 :::"min"::: )   "(" "a" "," "b" ")" ) ->   ($#v1_xxreal_0 :::"ext-real"::: )   ; 

cluster (Set   ($#k4_xxreal_0 :::"max"::: )   "(" "a" "," "b" ")" ) ->   ($#v1_xxreal_0 :::"ext-real"::: )   ; 
end; 
theorem :: XXREAL_0:17 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a")))) ; 
 
theorem :: XXREAL_0:18 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "d")))) "holds"  (Bool (Set   ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "a")) "," (Set (Var "c")) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "b")) "," (Set (Var "d")) ")" ))) ; 
 
theorem :: XXREAL_0:19 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "d")))) "holds"  (Bool (Set   ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "a")) "," (Set (Var "c")) ")" )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "b")) "," (Set (Var "d")) ")" ))) ; 
 
theorem :: XXREAL_0:20 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "c")))) "holds"  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "b")) "," (Set (Var "c")) ")" ))) ; 
 
theorem :: XXREAL_0:21 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "c")))) "holds"  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "b")) "," (Set (Var "c")) ")" ))) ; 
 
theorem :: XXREAL_0:22 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "b")) "," (Set (Var "c")) ")" ))) "holds"  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) ; 
 
theorem :: XXREAL_0:23 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "b")) "," (Set (Var "c")) ")" ))) "holds"  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b")))) ; 
 
theorem :: XXREAL_0:24 (Bool  "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool  "("   "for" (Set (Var "d")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "d"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set (Var "d"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) "holds"  (Bool (Set (Var "d"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "c")))  ")" )) "holds"  (Bool (Set (Var "c"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) ; 
 
theorem :: XXREAL_0:25 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) ; 
 
theorem :: XXREAL_0:26 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "d")))) "holds"  (Bool (Set   ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "a")) "," (Set (Var "c")) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "b")) "," (Set (Var "d")) ")" ))) ; 
 
theorem :: XXREAL_0:27 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "d")))) "holds"  (Bool (Set   ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "a")) "," (Set (Var "c")) ")" )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "b")) "," (Set (Var "d")) ")" ))) ; 
 
theorem :: XXREAL_0:28 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a")))) "holds"  (Bool (Set   ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "b")) "," (Set (Var "c")) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a")))) ; 
 
theorem :: XXREAL_0:29 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a"))) & (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a")))) "holds"  (Bool (Set   ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "b")) "," (Set (Var "c")) ")" )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a")))) ; 
 
theorem :: XXREAL_0:30 (Bool  "for" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "b")) "," (Set (Var "c")) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a")))) "holds"  (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a")))) ; 
 
theorem :: XXREAL_0:31 (Bool  "for" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "b")) "," (Set (Var "c")) ")" )  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a")))) "holds"  (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "a")))) ; 
 
theorem :: XXREAL_0:32 (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "c"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "c"))) & (Bool  "("   "for" (Set (Var "d")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "d"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "d")))) "holds"  (Bool (Set (Var "c"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "d")))  ")" )) "holds"  (Bool (Set (Var "c"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) ; 
 
theorem :: XXREAL_0:33 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k3_xxreal_0 :::"min"::: )   "(" (Set  "("  ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set (Var "c")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "a")) "," (Set  "("  ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "b")) "," (Set (Var "c")) ")"  ")" ) ")" ))) ; 
 
theorem :: XXREAL_0:34 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_xxreal_0 :::"max"::: )   "(" (Set  "("  ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set (Var "c")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "a")) "," (Set  "("  ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "b")) "," (Set (Var "c")) ")"  ")" ) ")" ))) ; 
 
theorem :: XXREAL_0:35 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k3_xxreal_0 :::"min"::: )   "(" (Set  "("  ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "b")))) ; 
 
theorem :: XXREAL_0:36 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_xxreal_0 :::"max"::: )   "(" (Set  "("  ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "b")))) ; 
 
theorem :: XXREAL_0:37 (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "c")))) "holds"  (Bool (Set   ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "a")) "," (Set  "("  ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "b")) "," (Set (Var "c")) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_xxreal_0 :::"min"::: )   "(" (Set  "("  ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set (Var "c")) ")" ))) ; 
 
theorem :: XXREAL_0:38 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "a")) "," (Set  "("  ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "b")) "," (Set (Var "c")) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_xxreal_0 :::"max"::: )   "(" (Set  "("  ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set  "("  ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "a")) "," (Set (Var "c")) ")"  ")" ) ")" ))) ; 
 
theorem :: XXREAL_0:39 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "a")) "," (Set  "("  ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "b")) "," (Set (Var "c")) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_xxreal_0 :::"min"::: )   "(" (Set  "("  ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set  "("  ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "a")) "," (Set (Var "c")) ")"  ")" ) ")" ))) ; 
 
theorem :: XXREAL_0:40 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_xxreal_0 :::"max"::: )   "(" (Set  "("  ($#k4_xxreal_0 :::"max"::: )   "(" (Set  "("  ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set  "("  ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "b")) "," (Set (Var "c")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "c")) "," (Set (Var "a")) ")"  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_xxreal_0 :::"min"::: )   "(" (Set  "("  ($#k3_xxreal_0 :::"min"::: )   "(" (Set  "("  ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ) "," (Set  "("  ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "b")) "," (Set (Var "c")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "c")) "," (Set (Var "a")) ")"  ")" ) ")" ))) ; 
 
theorem :: XXREAL_0:41 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "a")) "," (Set  ($#k1_xxreal_0 :::"+infty"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))) ; 
 
theorem :: XXREAL_0:42 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "a")) "," (Set  ($#k1_xxreal_0 :::"+infty"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 
theorem :: XXREAL_0:43 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "a")) "," (Set  ($#k2_xxreal_0 :::"-infty"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 
theorem :: XXREAL_0:44 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "a")) "," (Set  ($#k2_xxreal_0 :::"-infty"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_0 :::"-infty"::: )  ))) ; 
 begin  
theorem :: XXREAL_0:45 (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  )) & (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  )) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "c")))) "holds"  (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))) ; 
 
theorem :: XXREAL_0:46 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  )) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "c")))) "holds"  (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))) ; 
 
theorem :: XXREAL_0:47 (Bool  "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  )) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "c")))) "holds"  (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))) ; 
 
theorem :: XXREAL_0:48 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "c")))) "holds"  (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_numbers :::"REAL"::: )  ))) ; 
 definitionlet "x", "y" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )  ; let "a", "b" be    ($#m1_hidden :::"set"::: )  ; func  :::"IFGT":::  "(" "x" "," "y" "," "a" "," "b" ")"  ->    ($#m1_hidden :::"set"::: )   equals :: XXREAL_0:def 11 "a" if (Bool "x"  ($#r1_xxreal_0 :::">"::: )  "y")  otherwise "b"; end; 








:: deftheorem    defines :::"IFGT"::: XXREAL_0:def 11 :  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "x"))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "y")))) "implies" (Bool (Set   ($#k5_xxreal_0 :::"IFGT"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "x"))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "y"))))) "implies" (Bool (Set   ($#k5_xxreal_0 :::"IFGT"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")"   ")" ))); 
 registrationlet "x", "y" be   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )  ; let "a", "b" be   ($#m1_hidden :::"Nat":::); 
cluster (Set   ($#k5_xxreal_0 :::"IFGT"::: )   "(" "x" "," "y" "," "a" "," "b" ")" ) ->   ($#v7_ordinal1 :::"natural"::: )   ; 
end; 
theorem :: XXREAL_0:49 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a")))) "holds"  (Bool (Set   ($#k4_xxreal_0 :::"max"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 
theorem :: XXREAL_0:50 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) "holds"  (Bool (Set   ($#k3_xxreal_0 :::"min"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ;