:: XXREAL_2 semantic presentation begin scheme :: XXREAL_2:sch 1 FinInter{ F1() -> ($#m1_hidden :::"Integer":::), F2() -> ($#m1_hidden :::"Integer":::), F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "{" (Set F3 "(" (Set (Var "i")) ")" ) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) : (Bool "(" (Bool (Set F1 "(" ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set F2 "(" ")" )) & (Bool P1[(Set (Var "i"))]) ")" ) "}" "is" ($#v1_finset_1 :::"finite"::: ) ) proof end; definitionlet "X" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; mode :::"UpperBound"::: "of" "X" -> ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) means :: XXREAL_2:def 1 (Bool "for" (Set (Var "x")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) it)); mode :::"LowerBound"::: "of" "X" -> ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) means :: XXREAL_2:def 2 (Bool "for" (Set (Var "x")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool it ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x")))); end; :: deftheorem defines :::"UpperBound"::: XXREAL_2:def 1 : (Bool "for" (Set (Var "X")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_xxreal_2 :::"UpperBound"::: ) "of" (Set (Var "X"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b2")))) ")" ))); :: deftheorem defines :::"LowerBound"::: XXREAL_2:def 2 : (Bool "for" (Set (Var "X")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_xxreal_2 :::"LowerBound"::: ) "of" (Set (Var "X"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "b2")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x")))) ")" ))); definitionlet "X" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; func :::"sup"::: "X" -> ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) means :: XXREAL_2:def 3 (Bool "(" (Bool it "is" ($#m1_xxreal_2 :::"UpperBound"::: ) "of" "X") & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_xxreal_2 :::"UpperBound"::: ) "of" "X" "holds" (Bool it ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x"))) ")" ) ")" ); func :::"inf"::: "X" -> ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) means :: XXREAL_2:def 4 (Bool "(" (Bool it "is" ($#m2_xxreal_2 :::"LowerBound"::: ) "of" "X") & (Bool "(" "for" (Set (Var "x")) "being" ($#m2_xxreal_2 :::"LowerBound"::: ) "of" "X" "holds" (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) it) ")" ) ")" ); end; :: deftheorem defines :::"sup"::: XXREAL_2:def 3 : (Bool "for" (Set (Var "X")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_xxreal_2 :::"sup"::: ) (Set (Var "X")))) "iff" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_xxreal_2 :::"UpperBound"::: ) "of" (Set (Var "X"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_xxreal_2 :::"UpperBound"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Var "b2")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x"))) ")" ) ")" ) ")" ))); :: deftheorem defines :::"inf"::: XXREAL_2:def 4 : (Bool "for" (Set (Var "X")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "X")))) "iff" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_xxreal_2 :::"LowerBound"::: ) "of" (Set (Var "X"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m2_xxreal_2 :::"LowerBound"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b2"))) ")" ) ")" ) ")" ))); definitionlet "X" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; attr "X" is :::"left_end"::: means :: XXREAL_2:def 5 (Bool (Set ($#k2_xxreal_2 :::"inf"::: ) "X") ($#r2_hidden :::"in"::: ) "X"); attr "X" is :::"right_end"::: means :: XXREAL_2:def 6 (Bool (Set ($#k1_xxreal_2 :::"sup"::: ) "X") ($#r2_hidden :::"in"::: ) "X"); end; :: deftheorem defines :::"left_end"::: XXREAL_2:def 5 : (Bool "for" (Set (Var "X")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_xxreal_2 :::"left_end"::: ) ) "iff" (Bool (Set ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )); :: deftheorem defines :::"right_end"::: XXREAL_2:def 6 : (Bool "for" (Set (Var "X")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v2_xxreal_2 :::"right_end"::: ) ) "iff" (Bool (Set ($#k1_xxreal_2 :::"sup"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" )); theorem :: XXREAL_2:1 (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "y")) "is" ($#m1_xxreal_2 :::"UpperBound"::: ) "of" (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) "iff" (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "y"))) ")" )) ; theorem :: XXREAL_2:2 (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "y")) "is" ($#m2_xxreal_2 :::"LowerBound"::: ) "of" (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) "iff" (Bool (Set (Var "y")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x"))) ")" )) ; registration cluster -> ($#v2_membered :::"ext-real-membered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set ($#k7_numbers :::"ExtREAL"::: ) )); end; theorem :: XXREAL_2:3 (Bool "for" (Set (Var "x")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "A")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x"))))) ; theorem :: XXREAL_2:4 (Bool "for" (Set (Var "x")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "A")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_xxreal_2 :::"sup"::: ) (Set (Var "A")))))) ; theorem :: XXREAL_2:5 (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m2_xxreal_2 :::"LowerBound"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Var "x")) "is" ($#m2_xxreal_2 :::"LowerBound"::: ) "of" (Set (Var "B"))))) ; theorem :: XXREAL_2:6 (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_xxreal_2 :::"UpperBound"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Var "x")) "is" ($#m1_xxreal_2 :::"UpperBound"::: ) "of" (Set (Var "B"))))) ; theorem :: XXREAL_2:7 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_xxreal_2 :::"LowerBound"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "y")) "being" ($#m2_xxreal_2 :::"LowerBound"::: ) "of" (Set (Var "B")) "holds" (Bool (Set ($#k3_xxreal_0 :::"min"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) "is" ($#m2_xxreal_2 :::"LowerBound"::: ) "of" (Set (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B"))))))) ; theorem :: XXREAL_2:8 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_xxreal_2 :::"UpperBound"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "y")) "being" ($#m1_xxreal_2 :::"UpperBound"::: ) "of" (Set (Var "B")) "holds" (Bool (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) "is" ($#m1_xxreal_2 :::"UpperBound"::: ) "of" (Set (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B"))))))) ; theorem :: XXREAL_2:9 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_xxreal_2 :::"inf"::: ) (Set "(" (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_xxreal_0 :::"min"::: ) "(" (Set "(" ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "B")) ")" ) ")" ))) ; theorem :: XXREAL_2:10 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_xxreal_2 :::"sup"::: ) (Set "(" (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set "(" ($#k1_xxreal_2 :::"sup"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_xxreal_2 :::"sup"::: ) (Set (Var "B")) ")" ) ")" ))) ; registration cluster ($#v2_membered :::"ext-real-membered"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) -> ($#v2_membered :::"ext-real-membered"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_xxreal_2 :::"left_end"::: ) ($#v2_xxreal_2 :::"right_end"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v6_membered :::"natural-membered"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) -> ($#v6_membered :::"natural-membered"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_xxreal_2 :::"left_end"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_membered :::"complex-membered"::: ) ($#v2_membered :::"ext-real-membered"::: ) ($#v3_membered :::"real-membered"::: ) ($#v4_membered :::"rational-membered"::: ) ($#v5_membered :::"integer-membered"::: ) ($#v6_membered :::"natural-membered"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_xxreal_2 :::"left_end"::: ) ($#v2_xxreal_2 :::"right_end"::: ) for ($#m1_hidden :::"set"::: ) ; end; notationlet "X" be ($#v2_membered :::"ext-real-membered"::: ) ($#v1_xxreal_2 :::"left_end"::: ) ($#m1_hidden :::"set"::: ) ; synonym :::"min"::: "X" for :::"inf"::: "X"; end; notationlet "X" be ($#v2_membered :::"ext-real-membered"::: ) ($#v2_xxreal_2 :::"right_end"::: ) ($#m1_hidden :::"set"::: ) ; synonym :::"max"::: "X" for :::"sup"::: "X"; end; definitionlet "X" be ($#v2_membered :::"ext-real-membered"::: ) ($#v1_xxreal_2 :::"left_end"::: ) ($#m1_hidden :::"set"::: ) ; redefine func :::"inf"::: "X" means :: XXREAL_2:def 7 (Bool "(" (Bool it ($#r2_hidden :::"in"::: ) "X") & (Bool "(" "for" (Set (Var "x")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool it ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x"))) ")" ) ")" ); end; :: deftheorem defines :::"inf"::: XXREAL_2:def 7 : (Bool "for" (Set (Var "X")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#v1_xxreal_2 :::"left_end"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "X")))) "iff" (Bool "(" (Bool (Set (Var "b2")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "b2")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x"))) ")" ) ")" ) ")" ))); definitionlet "X" be ($#v2_membered :::"ext-real-membered"::: ) ($#v2_xxreal_2 :::"right_end"::: ) ($#m1_hidden :::"set"::: ) ; redefine func :::"sup"::: "X" means :: XXREAL_2:def 8 (Bool "(" (Bool it ($#r2_hidden :::"in"::: ) "X") & (Bool "(" "for" (Set (Var "x")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) it) ")" ) ")" ); end; :: deftheorem defines :::"sup"::: XXREAL_2:def 8 : (Bool "for" (Set (Var "X")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#v2_xxreal_2 :::"right_end"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_xxreal_2 :::"sup"::: ) (Set (Var "X")))) "iff" (Bool "(" (Bool (Set (Var "b2")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b2"))) ")" ) ")" ) ")" ))); theorem :: XXREAL_2:11 (Bool "for" (Set (Var "x")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_xxreal_2 :::"max"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ; theorem :: XXREAL_2:12 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xxreal_2 :::"max"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )))) ; theorem :: XXREAL_2:13 (Bool "for" (Set (Var "x")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k2_xxreal_2 :::"min"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ; theorem :: XXREAL_2:14 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k2_xxreal_2 :::"min"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k3_xxreal_0 :::"min"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))) ; definitionlet "X" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; attr "X" is :::"bounded_below"::: means :: XXREAL_2:def 9 (Bool "ex" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Set (Var "r")) "is" ($#m2_xxreal_2 :::"LowerBound"::: ) "of" "X")); attr "X" is :::"bounded_above"::: means :: XXREAL_2:def 10 (Bool "ex" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Set (Var "r")) "is" ($#m1_xxreal_2 :::"UpperBound"::: ) "of" "X")); end; :: deftheorem defines :::"bounded_below"::: XXREAL_2:def 9 : (Bool "for" (Set (Var "X")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ) "iff" (Bool "ex" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Set (Var "r")) "is" ($#m2_xxreal_2 :::"LowerBound"::: ) "of" (Set (Var "X")))) ")" )); :: deftheorem defines :::"bounded_above"::: XXREAL_2:def 10 : (Bool "for" (Set (Var "X")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ) "iff" (Bool "ex" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Set (Var "r")) "is" ($#m1_xxreal_2 :::"UpperBound"::: ) "of" (Set (Var "X")))) ")" )); registration cluster ($#v6_membered :::"natural-membered"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "X" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; attr "X" is :::"real-bounded"::: means :: XXREAL_2:def 11 (Bool "(" (Bool "X" "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ) & (Bool "X" "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ) ")" ); end; :: deftheorem defines :::"real-bounded"::: XXREAL_2:def 11 : (Bool "for" (Set (Var "X")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v5_xxreal_2 :::"real-bounded"::: ) ) "iff" (Bool "(" (Bool (Set (Var "X")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ) & (Bool (Set (Var "X")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ) ")" ) ")" )); registration cluster ($#v2_membered :::"ext-real-membered"::: ) ($#v5_xxreal_2 :::"real-bounded"::: ) -> ($#v2_membered :::"ext-real-membered"::: ) ($#v3_xxreal_2 :::"bounded_below"::: ) ($#v4_xxreal_2 :::"bounded_above"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v2_membered :::"ext-real-membered"::: ) ($#v3_xxreal_2 :::"bounded_below"::: ) ($#v4_xxreal_2 :::"bounded_above"::: ) -> ($#v2_membered :::"ext-real-membered"::: ) ($#v5_xxreal_2 :::"real-bounded"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v3_membered :::"real-membered"::: ) ($#v1_finset_1 :::"finite"::: ) -> ($#v3_membered :::"real-membered"::: ) ($#v5_xxreal_2 :::"real-bounded"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_membered :::"complex-membered"::: ) ($#v2_membered :::"ext-real-membered"::: ) ($#v3_membered :::"real-membered"::: ) ($#v4_membered :::"rational-membered"::: ) ($#v5_membered :::"integer-membered"::: ) ($#v6_membered :::"natural-membered"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_xxreal_2 :::"left_end"::: ) ($#v5_xxreal_2 :::"real-bounded"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: XXREAL_2:15 (Bool "for" (Set (Var "X")) "being" ($#v3_membered :::"real-membered"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) )) "holds" (Bool (Set ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) ; theorem :: XXREAL_2:16 (Bool "for" (Set (Var "X")) "being" ($#v3_membered :::"real-membered"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) )) "holds" (Bool (Set ($#k1_xxreal_2 :::"sup"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) ; registrationlet "X" be ($#v3_membered :::"real-membered"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_xxreal_2 :::"bounded_above"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_xxreal_2 :::"sup"::: ) "X") -> ($#v1_xxreal_0 :::"ext-real"::: ) ($#v1_xreal_0 :::"real"::: ) ; end; registrationlet "X" be ($#v3_membered :::"real-membered"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_xxreal_2 :::"bounded_below"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_xxreal_2 :::"inf"::: ) "X") -> ($#v1_xxreal_0 :::"ext-real"::: ) ($#v1_xreal_0 :::"real"::: ) ; end; registration cluster ($#v5_membered :::"integer-membered"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_xxreal_2 :::"bounded_above"::: ) -> ($#v5_membered :::"integer-membered"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_xxreal_2 :::"right_end"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v5_membered :::"integer-membered"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_xxreal_2 :::"bounded_below"::: ) -> ($#v5_membered :::"integer-membered"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_xxreal_2 :::"left_end"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v6_membered :::"natural-membered"::: ) -> ($#v6_membered :::"natural-membered"::: ) ($#v3_xxreal_2 :::"bounded_below"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X" be ($#v3_membered :::"real-membered"::: ) ($#v1_xxreal_2 :::"left_end"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_xxreal_2 :::"inf"::: ) "X") -> ($#v1_xxreal_0 :::"ext-real"::: ) ($#v1_xreal_0 :::"real"::: ) ; end; registrationlet "X" be ($#v4_membered :::"rational-membered"::: ) ($#v1_xxreal_2 :::"left_end"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_xxreal_2 :::"inf"::: ) "X") -> ($#v1_xxreal_0 :::"ext-real"::: ) ($#v1_rat_1 :::"rational"::: ) ; end; registrationlet "X" be ($#v5_membered :::"integer-membered"::: ) ($#v1_xxreal_2 :::"left_end"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_xxreal_2 :::"inf"::: ) "X") -> ($#v1_xxreal_0 :::"ext-real"::: ) ($#v1_int_1 :::"integer"::: ) ; end; registrationlet "X" be ($#v6_membered :::"natural-membered"::: ) ($#v1_xxreal_2 :::"left_end"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_xxreal_2 :::"inf"::: ) "X") -> ($#v1_xxreal_0 :::"ext-real"::: ) ($#v7_ordinal1 :::"natural"::: ) ; end; registrationlet "X" be ($#v3_membered :::"real-membered"::: ) ($#v2_xxreal_2 :::"right_end"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_xxreal_2 :::"sup"::: ) "X") -> ($#v1_xxreal_0 :::"ext-real"::: ) ($#v1_xreal_0 :::"real"::: ) ; end; registrationlet "X" be ($#v4_membered :::"rational-membered"::: ) ($#v2_xxreal_2 :::"right_end"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_xxreal_2 :::"sup"::: ) "X") -> ($#v1_xxreal_0 :::"ext-real"::: ) ($#v1_rat_1 :::"rational"::: ) ; end; registrationlet "X" be ($#v5_membered :::"integer-membered"::: ) ($#v2_xxreal_2 :::"right_end"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_xxreal_2 :::"sup"::: ) "X") -> ($#v1_xxreal_0 :::"ext-real"::: ) ($#v1_int_1 :::"integer"::: ) ; end; registrationlet "X" be ($#v6_membered :::"natural-membered"::: ) ($#v2_xxreal_2 :::"right_end"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_xxreal_2 :::"sup"::: ) "X") -> ($#v1_xxreal_0 :::"ext-real"::: ) ($#v7_ordinal1 :::"natural"::: ) ; end; registration cluster ($#v3_membered :::"real-membered"::: ) ($#v1_xxreal_2 :::"left_end"::: ) -> ($#v3_membered :::"real-membered"::: ) ($#v3_xxreal_2 :::"bounded_below"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v3_membered :::"real-membered"::: ) ($#v2_xxreal_2 :::"right_end"::: ) -> ($#v3_membered :::"real-membered"::: ) ($#v4_xxreal_2 :::"bounded_above"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: XXREAL_2:17 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Var "x")) "is" ($#m2_xxreal_2 :::"LowerBound"::: ) "of" (Set ($#k1_xxreal_1 :::"[."::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_xxreal_1 :::".]"::: ) ))) ; theorem :: XXREAL_2:18 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Var "x")) "is" ($#m2_xxreal_2 :::"LowerBound"::: ) "of" (Set ($#k3_xxreal_1 :::"]."::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k3_xxreal_1 :::".]"::: ) ))) ; theorem :: XXREAL_2:19 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Var "x")) "is" ($#m2_xxreal_2 :::"LowerBound"::: ) "of" (Set ($#k2_xxreal_1 :::"[."::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_xxreal_1 :::".["::: ) ))) ; theorem :: XXREAL_2:20 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Var "x")) "is" ($#m2_xxreal_2 :::"LowerBound"::: ) "of" (Set ($#k4_xxreal_1 :::"]."::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_xxreal_1 :::".["::: ) ))) ; theorem :: XXREAL_2:21 (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Var "y")) "is" ($#m1_xxreal_2 :::"UpperBound"::: ) "of" (Set ($#k1_xxreal_1 :::"[."::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_xxreal_1 :::".]"::: ) ))) ; theorem :: XXREAL_2:22 (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Var "y")) "is" ($#m1_xxreal_2 :::"UpperBound"::: ) "of" (Set ($#k3_xxreal_1 :::"]."::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k3_xxreal_1 :::".]"::: ) ))) ; theorem :: XXREAL_2:23 (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Var "y")) "is" ($#m1_xxreal_2 :::"UpperBound"::: ) "of" (Set ($#k2_xxreal_1 :::"[."::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_xxreal_1 :::".["::: ) ))) ; theorem :: XXREAL_2:24 (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Var "y")) "is" ($#m1_xxreal_2 :::"UpperBound"::: ) "of" (Set ($#k4_xxreal_1 :::"]."::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_xxreal_1 :::".["::: ) ))) ; theorem :: XXREAL_2:25 (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 ($#k2_xxreal_2 :::"inf"::: ) (Set ($#k1_xxreal_1 :::"[."::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_xxreal_1 :::".]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ; theorem :: XXREAL_2:26 (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 ($#k2_xxreal_2 :::"inf"::: ) (Set ($#k2_xxreal_1 :::"[."::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_xxreal_1 :::".["::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ; theorem :: XXREAL_2:27 (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 ($#k2_xxreal_2 :::"inf"::: ) (Set ($#k3_xxreal_1 :::"]."::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k3_xxreal_1 :::".]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ; theorem :: XXREAL_2:28 (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 ($#k2_xxreal_2 :::"inf"::: ) (Set ($#k4_xxreal_1 :::"]."::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_xxreal_1 :::".["::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "x")))) ; theorem :: XXREAL_2:29 (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 ($#k1_xxreal_2 :::"sup"::: ) (Set ($#k1_xxreal_1 :::"[."::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_xxreal_1 :::".]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "y")))) ; theorem :: XXREAL_2:30 (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 ($#k1_xxreal_2 :::"sup"::: ) (Set ($#k3_xxreal_1 :::"]."::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k3_xxreal_1 :::".]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "y")))) ; theorem :: XXREAL_2:31 (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 ($#k1_xxreal_2 :::"sup"::: ) (Set ($#k2_xxreal_1 :::"[."::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_xxreal_1 :::".["::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "y")))) ; theorem :: XXREAL_2:32 (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 ($#k1_xxreal_2 :::"sup"::: ) (Set ($#k4_xxreal_1 :::"]."::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_xxreal_1 :::".["::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "y")))) ; theorem :: XXREAL_2:33 (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 "(" (Bool (Set ($#k1_xxreal_1 :::"[."::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_xxreal_1 :::".]"::: ) ) "is" ($#v1_xxreal_2 :::"left_end"::: ) ) & (Bool (Set ($#k1_xxreal_1 :::"[."::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_xxreal_1 :::".]"::: ) ) "is" ($#v2_xxreal_2 :::"right_end"::: ) ) ")" )) ; theorem :: XXREAL_2:34 (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 ($#k2_xxreal_1 :::"[."::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_xxreal_1 :::".["::: ) ) "is" ($#v1_xxreal_2 :::"left_end"::: ) )) ; theorem :: XXREAL_2:35 (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 ($#k3_xxreal_1 :::"]."::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k3_xxreal_1 :::".]"::: ) ) "is" ($#v2_xxreal_2 :::"right_end"::: ) )) ; theorem :: XXREAL_2:36 (Bool "for" (Set (Var "x")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Var "x")) "is" ($#m2_xxreal_2 :::"LowerBound"::: ) "of" (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: XXREAL_2:37 (Bool "for" (Set (Var "x")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Var "x")) "is" ($#m1_xxreal_2 :::"UpperBound"::: ) "of" (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: XXREAL_2:38 (Bool (Set ($#k2_xxreal_2 :::"inf"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xxreal_0 :::"+infty"::: ) )) ; theorem :: XXREAL_2:39 (Bool (Set ($#k1_xxreal_2 :::"sup"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) )) ; theorem :: XXREAL_2:40 (Bool "for" (Set (Var "X")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) )) "iff" (Bool (Set ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "X"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_xxreal_2 :::"sup"::: ) (Set (Var "X")))) ")" )) ; registration cluster ($#v5_membered :::"integer-membered"::: ) ($#v5_xxreal_2 :::"real-bounded"::: ) -> ($#v5_membered :::"integer-membered"::: ) ($#v1_finset_1 :::"finite"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v6_membered :::"natural-membered"::: ) ($#v4_xxreal_2 :::"bounded_above"::: ) -> ($#v6_membered :::"natural-membered"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v4_xxreal_2 :::"bounded_above"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: XXREAL_2:41 (Bool "for" (Set (Var "X")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_xxreal_0 :::"+infty"::: ) ) "is" ($#m1_xxreal_2 :::"UpperBound"::: ) "of" (Set (Var "X")))) ; theorem :: XXREAL_2:42 (Bool "for" (Set (Var "X")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "is" ($#m2_xxreal_2 :::"LowerBound"::: ) "of" (Set (Var "X")))) ; theorem :: XXREAL_2:43 (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"))) & (Bool (Set (Var "Y")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) )) "holds" (Bool (Set (Var "X")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) )) ; theorem :: XXREAL_2:44 (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"))) & (Bool (Set (Var "Y")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) )) "holds" (Bool (Set (Var "X")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) )) ; theorem :: XXREAL_2:45 (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"))) & (Bool (Set (Var "Y")) "is" ($#v5_xxreal_2 :::"real-bounded"::: ) )) "holds" (Bool (Set (Var "X")) "is" ($#v5_xxreal_2 :::"real-bounded"::: ) )) ; theorem :: XXREAL_2:46 (Bool "(" (Bool (Bool "not" (Set ($#k1_numbers :::"REAL"::: ) ) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) )) & (Bool (Bool "not" (Set ($#k1_numbers :::"REAL"::: ) ) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) )) ")" ) ; registration cluster (Set ($#k1_numbers :::"REAL"::: ) ) -> ($#~v3_xxreal_2 "non" ($#v3_xxreal_2 :::"bounded_below"::: ) ) ($#~v4_xxreal_2 "non" ($#v4_xxreal_2 :::"bounded_above"::: ) ) ; end; theorem :: XXREAL_2:47 (Bool (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k1_tarski :::"}"::: ) ) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ) ; theorem :: XXREAL_2:48 (Bool (Set ($#k1_tarski :::"{"::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) ($#k1_tarski :::"}"::: ) ) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ) ; theorem :: XXREAL_2:49 (Bool "for" (Set (Var "X")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_xxreal_2 :::"bounded_above"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) ; theorem :: XXREAL_2:50 (Bool "for" (Set (Var "X")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_xxreal_2 :::"bounded_below"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) ; theorem :: XXREAL_2:51 (Bool "for" (Set (Var "X")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "is" ($#m1_xxreal_2 :::"UpperBound"::: ) "of" (Set (Var "X")))) "holds" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: XXREAL_2:52 (Bool "for" (Set (Var "X")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k1_xxreal_0 :::"+infty"::: ) ) "is" ($#m2_xxreal_2 :::"LowerBound"::: ) "of" (Set (Var "X")))) "holds" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: XXREAL_2:53 (Bool "for" (Set (Var "X")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "ex" (Set (Var "y")) "being" ($#m1_xxreal_2 :::"UpperBound"::: ) "of" (Set (Var "X")) "st" (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xxreal_0 :::"+infty"::: ) )))) "holds" (Bool (Set (Var "X")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) )) ; theorem :: XXREAL_2:54 (Bool "for" (Set (Var "X")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "ex" (Set (Var "y")) "being" ($#m2_xxreal_2 :::"LowerBound"::: ) "of" (Set (Var "X")) "st" (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) )))) "holds" (Bool (Set (Var "X")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) )) ; theorem :: XXREAL_2:55 (Bool "for" (Set (Var "X")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_xxreal_2 :::"UpperBound"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_xxreal_2 :::"sup"::: ) (Set (Var "X")))))) ; theorem :: XXREAL_2:56 (Bool "for" (Set (Var "X")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_xxreal_2 :::"LowerBound"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "X")))))) ; theorem :: XXREAL_2:57 (Bool "for" (Set (Var "X")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ) & (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set ($#k1_xxreal_2 :::"sup"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) ; theorem :: XXREAL_2:58 (Bool "for" (Set (Var "X")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ) & (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "X"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) ; theorem :: XXREAL_2:59 (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 (Set ($#k1_xxreal_2 :::"sup"::: ) (Set (Var "X"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_xxreal_2 :::"sup"::: ) (Set (Var "Y"))))) ; theorem :: XXREAL_2:60 (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 (Set ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "Y"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "X"))))) ; theorem :: XXREAL_2:61 (Bool "for" (Set (Var "X")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "ex" (Set (Var "y")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "y"))) ")" ))) "holds" (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_xxreal_2 :::"sup"::: ) (Set (Var "X")))))) ; theorem :: XXREAL_2:62 (Bool "for" (Set (Var "X")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "ex" (Set (Var "y")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x"))) ")" ))) "holds" (Bool (Set ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "X"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x"))))) ; theorem :: XXREAL_2:63 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "y"))) ")" )) ")" )) "holds" (Bool (Set ($#k1_xxreal_2 :::"sup"::: ) (Set (Var "X"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_xxreal_2 :::"sup"::: ) (Set (Var "Y"))))) ; theorem :: XXREAL_2:64 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "y")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "y"))) ")" )) ")" )) "holds" (Bool (Set ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "X"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "Y"))))) ; theorem :: XXREAL_2:65 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_xxreal_2 :::"UpperBound"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "y")) "being" ($#m1_xxreal_2 :::"UpperBound"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k3_xxreal_0 :::"min"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) "is" ($#m1_xxreal_2 :::"UpperBound"::: ) "of" (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y"))))))) ; theorem :: XXREAL_2:66 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_xxreal_2 :::"LowerBound"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "y")) "being" ($#m2_xxreal_2 :::"LowerBound"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) "is" ($#m2_xxreal_2 :::"LowerBound"::: ) "of" (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y"))))))) ; theorem :: XXREAL_2:67 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_xxreal_2 :::"sup"::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_xxreal_0 :::"min"::: ) "(" (Set "(" ($#k1_xxreal_2 :::"sup"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k1_xxreal_2 :::"sup"::: ) (Set (Var "Y")) ")" ) ")" ))) ; theorem :: XXREAL_2:68 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set "(" ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "Y")) ")" ) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_xxreal_2 :::"inf"::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" )))) ; registration cluster ($#v2_membered :::"ext-real-membered"::: ) ($#v5_xxreal_2 :::"real-bounded"::: ) -> ($#v2_membered :::"ext-real-membered"::: ) ($#v3_membered :::"real-membered"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: XXREAL_2:69 (Bool "for" (Set (Var "A")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k1_xxreal_1 :::"[."::: ) (Set "(" ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_xxreal_2 :::"sup"::: ) (Set (Var "A")) ")" ) ($#k1_xxreal_1 :::".]"::: ) ))) ; theorem :: XXREAL_2:70 (Bool "for" (Set (Var "A")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k1_xxreal_2 :::"sup"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "A")) ")" ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: XXREAL_2:71 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "A")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "y"))) & (Bool (Set (Var "x")) "is" ($#m1_xxreal_2 :::"UpperBound"::: ) "of" (Set (Var "A")))) "holds" (Bool (Set (Var "y")) "is" ($#m1_xxreal_2 :::"UpperBound"::: ) "of" (Set (Var "A"))))) ; theorem :: XXREAL_2:72 (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "A")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) "is" ($#m2_xxreal_2 :::"LowerBound"::: ) "of" (Set (Var "A")))) "holds" (Bool (Set (Var "y")) "is" ($#m2_xxreal_2 :::"LowerBound"::: ) "of" (Set (Var "A"))))) ; theorem :: XXREAL_2:73 (Bool "for" (Set (Var "A")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ) "iff" (Bool (Set ($#k1_xxreal_2 :::"sup"::: ) (Set (Var "A"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xxreal_0 :::"+infty"::: ) )) ")" )) ; theorem :: XXREAL_2:74 (Bool "for" (Set (Var "A")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ) "iff" (Bool (Set ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "A"))) ($#r1_hidden :::"<>"::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) )) ")" )) ; begin definitionlet "A" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; attr "A" is :::"interval"::: means :: XXREAL_2:def 12 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) "A") & (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) "A")) "holds" (Bool (Set ($#k1_xxreal_1 :::"[."::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k1_xxreal_1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) "A")); end; :: deftheorem defines :::"interval"::: XXREAL_2:def 12 : (Bool "for" (Set (Var "A")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v6_xxreal_2 :::"interval"::: ) ) "iff" (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k1_xxreal_1 :::"[."::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k1_xxreal_1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) ")" )); registration cluster (Set ($#k7_numbers :::"ExtREAL"::: ) ) -> ($#v6_xxreal_2 :::"interval"::: ) ; cluster ($#v2_membered :::"ext-real-membered"::: ) ($#v1_xboole_0 :::"empty"::: ) -> ($#v2_membered :::"ext-real-membered"::: ) ($#v6_xxreal_2 :::"interval"::: ) for ($#m1_hidden :::"set"::: ) ; let "r", "s" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k1_xxreal_1 :::"[."::: ) "r" "," "s" ($#k1_xxreal_1 :::".]"::: ) ) -> ($#v6_xxreal_2 :::"interval"::: ) ; cluster (Set ($#k3_xxreal_1 :::"]."::: ) "r" "," "s" ($#k3_xxreal_1 :::".]"::: ) ) -> ($#v6_xxreal_2 :::"interval"::: ) ; cluster (Set ($#k2_xxreal_1 :::"[."::: ) "r" "," "s" ($#k2_xxreal_1 :::".["::: ) ) -> ($#v6_xxreal_2 :::"interval"::: ) ; cluster (Set ($#k4_xxreal_1 :::"]."::: ) "r" "," "s" ($#k4_xxreal_1 :::".["::: ) ) -> ($#v6_xxreal_2 :::"interval"::: ) ; end; registration cluster (Set ($#k1_numbers :::"REAL"::: ) ) -> ($#v6_xxreal_2 :::"interval"::: ) ; end; registration cluster ($#v2_membered :::"ext-real-membered"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v6_xxreal_2 :::"interval"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "A", "B" be ($#v2_membered :::"ext-real-membered"::: ) ($#v6_xxreal_2 :::"interval"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "A" ($#k3_xboole_0 :::"/\"::: ) "B") -> ($#v6_xxreal_2 :::"interval"::: ) ; end; registrationlet "r", "s" be ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k3_xxreal_1 :::"]."::: ) "r" "," "s" ($#k3_xxreal_1 :::".]"::: ) ) -> ($#~v1_xxreal_2 "non" ($#v1_xxreal_2 :::"left_end"::: ) ) ; cluster (Set ($#k2_xxreal_1 :::"[."::: ) "r" "," "s" ($#k2_xxreal_1 :::".["::: ) ) -> ($#~v2_xxreal_2 "non" ($#v2_xxreal_2 :::"right_end"::: ) ) ; cluster (Set ($#k4_xxreal_1 :::"]."::: ) "r" "," "s" ($#k4_xxreal_1 :::".["::: ) ) -> ($#~v1_xxreal_2 "non" ($#v1_xxreal_2 :::"left_end"::: ) ) ($#~v2_xxreal_2 "non" ($#v2_xxreal_2 :::"right_end"::: ) ) ; end; registration cluster ($#v2_membered :::"ext-real-membered"::: ) ($#v1_xxreal_2 :::"left_end"::: ) ($#v2_xxreal_2 :::"right_end"::: ) ($#v6_xxreal_2 :::"interval"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v2_membered :::"ext-real-membered"::: ) ($#~v1_xxreal_2 "non" ($#v1_xxreal_2 :::"left_end"::: ) ) ($#v2_xxreal_2 :::"right_end"::: ) ($#v6_xxreal_2 :::"interval"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v2_membered :::"ext-real-membered"::: ) ($#v1_xxreal_2 :::"left_end"::: ) ($#~v2_xxreal_2 "non" ($#v2_xxreal_2 :::"right_end"::: ) ) ($#v6_xxreal_2 :::"interval"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v2_membered :::"ext-real-membered"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#~v1_xxreal_2 "non" ($#v1_xxreal_2 :::"left_end"::: ) ) ($#~v2_xxreal_2 "non" ($#v2_xxreal_2 :::"right_end"::: ) ) ($#v6_xxreal_2 :::"interval"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: XXREAL_2:75 (Bool "for" (Set (Var "A")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#v1_xxreal_2 :::"left_end"::: ) ($#v2_xxreal_2 :::"right_end"::: ) ($#v6_xxreal_2 :::"interval"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xxreal_1 :::"[."::: ) (Set "(" ($#k2_xxreal_2 :::"min"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_xxreal_2 :::"max"::: ) (Set (Var "A")) ")" ) ($#k1_xxreal_1 :::".]"::: ) ))) ; theorem :: XXREAL_2:76 (Bool "for" (Set (Var "A")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#~v1_xxreal_2 "non" ($#v1_xxreal_2 :::"left_end"::: ) ) ($#v2_xxreal_2 :::"right_end"::: ) ($#v6_xxreal_2 :::"interval"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k3_xxreal_1 :::"]."::: ) (Set "(" ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_xxreal_2 :::"max"::: ) (Set (Var "A")) ")" ) ($#k3_xxreal_1 :::".]"::: ) ))) ; theorem :: XXREAL_2:77 (Bool "for" (Set (Var "A")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#v1_xxreal_2 :::"left_end"::: ) ($#~v2_xxreal_2 "non" ($#v2_xxreal_2 :::"right_end"::: ) ) ($#v6_xxreal_2 :::"interval"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_xxreal_1 :::"[."::: ) (Set "(" ($#k2_xxreal_2 :::"min"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_xxreal_2 :::"sup"::: ) (Set (Var "A")) ")" ) ($#k2_xxreal_1 :::".["::: ) ))) ; theorem :: XXREAL_2:78 (Bool "for" (Set (Var "A")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#~v1_xxreal_2 "non" ($#v1_xxreal_2 :::"left_end"::: ) ) ($#~v2_xxreal_2 "non" ($#v2_xxreal_2 :::"right_end"::: ) ) ($#v6_xxreal_2 :::"interval"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k4_xxreal_1 :::"]."::: ) (Set "(" ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k1_xxreal_2 :::"sup"::: ) (Set (Var "A")) ")" ) ($#k4_xxreal_1 :::".["::: ) ))) ; theorem :: XXREAL_2:79 (Bool "for" (Set (Var "A")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#~v1_xxreal_2 "non" ($#v1_xxreal_2 :::"left_end"::: ) ) ($#~v2_xxreal_2 "non" ($#v2_xxreal_2 :::"right_end"::: ) ) ($#v6_xxreal_2 :::"interval"::: ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "r")) "," (Set (Var "s")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k4_xxreal_1 :::"]."::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k4_xxreal_1 :::".["::: ) )) ")" ))) ; theorem :: XXREAL_2:80 (Bool "for" (Set (Var "A")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) "is" ($#v6_xxreal_2 :::"interval"::: ) )) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "r")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))))) ; theorem :: XXREAL_2:81 (Bool "for" (Set (Var "A")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) "is" ($#v6_xxreal_2 :::"interval"::: ) )) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "r")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_xxreal_2 :::"sup"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))))) ; theorem :: XXREAL_2:82 (Bool "for" (Set (Var "A")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) "is" ($#v6_xxreal_2 :::"interval"::: ) )) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "r")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x")))) "holds" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))))) ; theorem :: XXREAL_2:83 (Bool "for" (Set (Var "A")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) "is" ($#v6_xxreal_2 :::"interval"::: ) )) "holds" (Bool "for" (Set (Var "r")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_xxreal_2 :::"sup"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))))) ; theorem :: XXREAL_2:84 (Bool "for" (Set (Var "A")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "r")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) "holds" (Bool (Set (Var "A")) "is" ($#v6_xxreal_2 :::"interval"::: ) )) ; theorem :: XXREAL_2:85 (Bool "for" (Set (Var "A")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "," (Set (Var "r")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_xxreal_2 :::"sup"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) "holds" (Bool (Set (Var "A")) "is" ($#v6_xxreal_2 :::"interval"::: ) )) ; theorem :: XXREAL_2:86 (Bool "for" (Set (Var "A")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "y")) "," (Set (Var "r")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) "holds" (Bool (Set (Var "A")) "is" ($#v6_xxreal_2 :::"interval"::: ) )) ; theorem :: XXREAL_2:87 (Bool "for" (Set (Var "A")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "r")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_xxreal_2 :::"sup"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) "holds" (Bool (Set (Var "A")) "is" ($#v6_xxreal_2 :::"interval"::: ) )) ; theorem :: XXREAL_2:88 (Bool "for" (Set (Var "A")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "r")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) "holds" (Bool (Set (Var "A")) "is" ($#v6_xxreal_2 :::"interval"::: ) )) ; theorem :: XXREAL_2:89 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) "is" ($#v6_xxreal_2 :::"interval"::: ) ) & (Bool (Set (Var "B")) "is" ($#v6_xxreal_2 :::"interval"::: ) ) & (Bool (Set (Var "A")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B"))) "is" ($#v6_xxreal_2 :::"interval"::: ) )) ; theorem :: XXREAL_2:90 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) "is" ($#v6_xxreal_2 :::"interval"::: ) ) & (Bool (Set (Var "B")) "is" ($#v1_xxreal_2 :::"left_end"::: ) ) & (Bool (Set (Var "B")) "is" ($#v6_xxreal_2 :::"interval"::: ) ) & (Bool (Set ($#k1_xxreal_2 :::"sup"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B"))) "is" ($#v6_xxreal_2 :::"interval"::: ) )) ; theorem :: XXREAL_2:91 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) "is" ($#v2_xxreal_2 :::"right_end"::: ) ) & (Bool (Set (Var "A")) "is" ($#v6_xxreal_2 :::"interval"::: ) ) & (Bool (Set (Var "B")) "is" ($#v6_xxreal_2 :::"interval"::: ) ) & (Bool (Set ($#k1_xxreal_2 :::"sup"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B"))) "is" ($#v6_xxreal_2 :::"interval"::: ) )) ; registration cluster ($#v2_membered :::"ext-real-membered"::: ) ($#v1_xxreal_2 :::"left_end"::: ) -> ($#v2_membered :::"ext-real-membered"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v2_membered :::"ext-real-membered"::: ) ($#v2_xxreal_2 :::"right_end"::: ) -> ($#v2_membered :::"ext-real-membered"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: XXREAL_2:92 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) )) ")" )) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: XXREAL_2:93 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) ")" )) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: XXREAL_2:94 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_xxreal_2 :::"sup"::: ) (Set (Var "A"))))) "holds" (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "s"))) ")" )))) ; theorem :: XXREAL_2:95 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "holds" (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" )))) ; theorem :: XXREAL_2:96 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s"))) ")" )) "holds" (Bool (Set ($#k1_xxreal_2 :::"sup"::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_xxreal_2 :::"inf"::: ) (Set (Var "B"))))) ;