:: SUPINF_1  semantic presentation begin  definitionmode R_eal is    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k7_numbers :::"ExtREAL"::: )  ); end; definition:: original: :::"+infty"::: redefine func  :::"+infty":::  ->   ($#m1_subset_1 :::"R_eal":::); :: original: :::"-infty"::: redefine func  :::"-infty":::  ->   ($#m1_subset_1 :::"R_eal":::); end; definitionlet "X" be   ($#v2_membered :::"ext-real-membered"::: )     ($#m1_hidden :::"set"::: )  ; func  :::"SetMajorant"::: "X" ->   ($#v2_membered :::"ext-real-membered"::: )     ($#m1_hidden :::"set"::: )   means :: SUPINF_1:def 1 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool (Set (Var "x")) "is"    ($#m1_xxreal_2 :::"UpperBound"::: )   "of" "X")  ")" )); end; 





:: deftheorem    defines :::"SetMajorant"::: SUPINF_1:def 1 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "b2")) "being"   ($#v2_membered :::"ext-real-membered"::: )     ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_supinf_1 :::"SetMajorant"::: )  (Set (Var "X")))) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) "iff" (Bool (Set (Var "x")) "is"    ($#m1_xxreal_2 :::"UpperBound"::: )   "of" (Set (Var "X")))  ")" ))  ")" )); 
 registrationlet "X" be   ($#v2_membered :::"ext-real-membered"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k3_supinf_1 :::"SetMajorant"::: )  "X") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_membered :::"ext-real-membered"::: )   ; 
end; 
theorem :: SUPINF_1:1 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#v2_membered :::"ext-real-membered"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool  "for" (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_supinf_1 :::"SetMajorant"::: )  (Set (Var "Y"))))) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_supinf_1 :::"SetMajorant"::: )  (Set (Var "X")))))) ; 
 definitionlet "X" be   ($#v2_membered :::"ext-real-membered"::: )     ($#m1_hidden :::"set"::: )  ; func  :::"SetMinorant"::: "X" ->   ($#v2_membered :::"ext-real-membered"::: )     ($#m1_hidden :::"set"::: )   means :: SUPINF_1:def 2 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool (Set (Var "x")) "is"    ($#m2_xxreal_2 :::"LowerBound"::: )   "of" "X")  ")" )); end; 





:: deftheorem    defines :::"SetMinorant"::: SUPINF_1:def 2 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "b2")) "being"   ($#v2_membered :::"ext-real-membered"::: )     ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_supinf_1 :::"SetMinorant"::: )  (Set (Var "X")))) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) "iff" (Bool (Set (Var "x")) "is"    ($#m2_xxreal_2 :::"LowerBound"::: )   "of" (Set (Var "X")))  ")" ))  ")" )); 
 registrationlet "X" be   ($#v2_membered :::"ext-real-membered"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k4_supinf_1 :::"SetMinorant"::: )  "X") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_membered :::"ext-real-membered"::: )   ; 
end; 
theorem :: SUPINF_1:2 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#v2_membered :::"ext-real-membered"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool  "for" (Set (Var "x")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_supinf_1 :::"SetMinorant"::: )  (Set (Var "Y"))))) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_supinf_1 :::"SetMinorant"::: )  (Set (Var "X")))))) ; 
 
theorem :: SUPINF_1:3 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_membered :::"ext-real-membered"::: )     ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k1_xxreal_2 :::"sup"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_2 :::"inf"::: )  (Set  "("  ($#k3_supinf_1 :::"SetMajorant"::: )  (Set (Var "X")) ")" ))) & (Bool (Set   ($#k2_xxreal_2 :::"inf"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_2 :::"sup"::: )  (Set  "("  ($#k4_supinf_1 :::"SetMinorant"::: )  (Set (Var "X")) ")" )))  ")" )) ; 
 registrationlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_setfam_1 :::"with_non-empty_elements"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK1_ZFMISC_1("X")))); 
end; definitionlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; mode bool_DOMAIN of "X" is  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_setfam_1 :::"with_non-empty_elements"::: )    ($#m1_subset_1 :::"Subset-Family":::) "of" "X"; end; definitionlet "F" be   ($#m1_subset_1 :::"bool_DOMAIN":::) "of" (Set  ($#k7_numbers :::"ExtREAL"::: ) ); func  :::"SUP"::: "F" ->   ($#v2_membered :::"ext-real-membered"::: )     ($#m1_hidden :::"set"::: )   means :: SUPINF_1:def 3 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "ex" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_membered :::"ext-real-membered"::: )     ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  "F") & (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_2 :::"sup"::: )  (Set (Var "A"))))  ")" ))  ")" )); end; 





:: deftheorem    defines :::"SUP"::: SUPINF_1:def 3 :  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"bool_DOMAIN":::) "of" (Set  ($#k7_numbers :::"ExtREAL"::: ) )  (Bool  "for" (Set (Var "b2")) "being"   ($#v2_membered :::"ext-real-membered"::: )     ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_supinf_1 :::"SUP"::: )  (Set (Var "F")))) "iff" (Bool  "for" (Set (Var "a")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) "iff" (Bool  "ex" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_membered :::"ext-real-membered"::: )     ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "F"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_2 :::"sup"::: )  (Set (Var "A"))))  ")" ))  ")" ))  ")" ))); 
 registrationlet "F" be   ($#m1_subset_1 :::"bool_DOMAIN":::) "of" (Set  ($#k7_numbers :::"ExtREAL"::: ) ); 
cluster (Set   ($#k5_supinf_1 :::"SUP"::: )  "F") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_membered :::"ext-real-membered"::: )   ; 
end; 
theorem :: SUPINF_1:4 (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"bool_DOMAIN":::) "of" (Set  ($#k7_numbers :::"ExtREAL"::: ) )  (Bool  "for" (Set (Var "S")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_membered :::"ext-real-membered"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "S"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_setfam_1 :::"union"::: )  (Set (Var "F"))))) "holds"  (Bool (Set   ($#k1_xxreal_2 :::"sup"::: )  (Set (Var "S"))) "is"    ($#m1_xxreal_2 :::"UpperBound"::: )   "of" (Set   ($#k5_supinf_1 :::"SUP"::: )  (Set (Var "F")))))) ; 
 
theorem :: SUPINF_1:5 (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"bool_DOMAIN":::) "of" (Set  ($#k7_numbers :::"ExtREAL"::: ) )  (Bool  "for" (Set (Var "S")) "being"   ($#v2_membered :::"ext-real-membered"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "S"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_setfam_1 :::"union"::: )  (Set (Var "F"))))) "holds"  (Bool (Set   ($#k1_xxreal_2 :::"sup"::: )  (Set  "("  ($#k5_supinf_1 :::"SUP"::: )  (Set (Var "F")) ")" )) "is"    ($#m1_xxreal_2 :::"UpperBound"::: )   "of" (Set (Var "S"))))) ; 
 
theorem :: SUPINF_1:6 (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"bool_DOMAIN":::) "of" (Set  ($#k7_numbers :::"ExtREAL"::: ) )  (Bool  "for" (Set (Var "S")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_membered :::"ext-real-membered"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "S"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_setfam_1 :::"union"::: )  (Set (Var "F"))))) "holds"  (Bool (Set   ($#k1_xxreal_2 :::"sup"::: )  (Set (Var "S")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_2 :::"sup"::: )  (Set  "("  ($#k5_supinf_1 :::"SUP"::: )  (Set (Var "F")) ")" ))))) ; 
 definitionlet "F" be   ($#m1_subset_1 :::"bool_DOMAIN":::) "of" (Set  ($#k7_numbers :::"ExtREAL"::: ) ); func  :::"INF"::: "F" ->   ($#v2_membered :::"ext-real-membered"::: )     ($#m1_hidden :::"set"::: )   means :: SUPINF_1:def 4 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "ex" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_membered :::"ext-real-membered"::: )     ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  "F") & (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_2 :::"inf"::: )  (Set (Var "A"))))  ")" ))  ")" )); end; 





:: deftheorem    defines :::"INF"::: SUPINF_1:def 4 :  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"bool_DOMAIN":::) "of" (Set  ($#k7_numbers :::"ExtREAL"::: ) )  (Bool  "for" (Set (Var "b2")) "being"   ($#v2_membered :::"ext-real-membered"::: )     ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_supinf_1 :::"INF"::: )  (Set (Var "F")))) "iff" (Bool  "for" (Set (Var "a")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) "iff" (Bool  "ex" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_membered :::"ext-real-membered"::: )     ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "F"))) & (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_2 :::"inf"::: )  (Set (Var "A"))))  ")" ))  ")" ))  ")" ))); 
 registrationlet "F" be   ($#m1_subset_1 :::"bool_DOMAIN":::) "of" (Set  ($#k7_numbers :::"ExtREAL"::: ) ); 
cluster (Set   ($#k6_supinf_1 :::"INF"::: )  "F") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_membered :::"ext-real-membered"::: )   ; 
end; 
theorem :: SUPINF_1:7 (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"bool_DOMAIN":::) "of" (Set  ($#k7_numbers :::"ExtREAL"::: ) )  (Bool  "for" (Set (Var "S")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_membered :::"ext-real-membered"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "S"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_setfam_1 :::"union"::: )  (Set (Var "F"))))) "holds"  (Bool (Set   ($#k2_xxreal_2 :::"inf"::: )  (Set (Var "S"))) "is"    ($#m2_xxreal_2 :::"LowerBound"::: )   "of" (Set   ($#k6_supinf_1 :::"INF"::: )  (Set (Var "F")))))) ; 
 
theorem :: SUPINF_1:8 (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"bool_DOMAIN":::) "of" (Set  ($#k7_numbers :::"ExtREAL"::: ) )  (Bool  "for" (Set (Var "S")) "being"   ($#v2_membered :::"ext-real-membered"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "S"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_setfam_1 :::"union"::: )  (Set (Var "F"))))) "holds"  (Bool (Set   ($#k2_xxreal_2 :::"inf"::: )  (Set  "("  ($#k6_supinf_1 :::"INF"::: )  (Set (Var "F")) ")" )) "is"    ($#m2_xxreal_2 :::"LowerBound"::: )   "of" (Set (Var "S"))))) ; 
 
theorem :: SUPINF_1:9 (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"bool_DOMAIN":::) "of" (Set  ($#k7_numbers :::"ExtREAL"::: ) )  (Bool  "for" (Set (Var "S")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_membered :::"ext-real-membered"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "S"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_setfam_1 :::"union"::: )  (Set (Var "F"))))) "holds"  (Bool (Set   ($#k2_xxreal_2 :::"inf"::: )  (Set (Var "S")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xxreal_2 :::"inf"::: )  (Set  "("  ($#k6_supinf_1 :::"INF"::: )  (Set (Var "F")) ")" ))))) ;