:: SETLIM_1 semantic presentation begin theorem :: SETLIM_1:1 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "Y")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "m")) ")" )) ($#r2_hidden :::"in"::: ) "{" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "k")) ")" ) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) "}" )))) ; theorem :: SETLIM_1:2 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "Y")) "holds" (Bool "{" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "k1")) ")" ) where k1 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k1"))) "}" ($#r1_hidden :::"="::: ) (Set "{" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "k2")) ")" ) where k2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k2"))) "}" ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_tarski :::"}"::: ) )))))) ; theorem :: SETLIM_1:3 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "Y")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "Y")) "holds" (Bool "(" (Bool "(" "for" (Set (Var "k1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k1")) ")" ))) ")" ) "iff" (Bool "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Z")) ($#r2_hidden :::"in"::: ) "{" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "k2")) ")" ) where k2 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k2"))) "}" )) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) ")" )))) ; theorem :: SETLIM_1:4 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")))) "iff" (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))))) ")" )))) ; theorem :: SETLIM_1:5 (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "Y")) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "k")) ")" ) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) "}" ))) ; theorem :: SETLIM_1:6 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "Y")) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k10_nat_1 :::"^\"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) where n "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) "}" )))) ; theorem :: SETLIM_1:7 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k6_setfam_1 :::"meet"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "B")) ")" ))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "B")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))))) ")" ))) ; theorem :: SETLIM_1:8 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k6_setfam_1 :::"meet"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "B")) ")" ))))) ; theorem :: SETLIM_1:9 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_kurato_0 :::"Union"::: ) (Set (Var "B")))))) ; theorem :: SETLIM_1:10 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "B")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) ")" )) "holds" (Bool (Set ($#k1_kurato_0 :::"Union"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))))) ; theorem :: SETLIM_1:11 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "B")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) ")" )) "holds" (Bool (Set ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))))) ; theorem :: SETLIM_1:12 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" ($#v3_funct_1 :::"constant"::: ) )) "holds" (Bool (Set ($#k1_kurato_0 :::"Union"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "B")))))) ; theorem :: SETLIM_1:13 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" ($#v3_funct_1 :::"constant"::: ) ) & (Bool (Set ($#k3_funct_1 :::"the_value_of"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set (Var "B")) ($#k3_funct_2 :::"."::: ) (Set (Var "k")) ")" ) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) "}" ) ($#r1_hidden :::"="::: ) (Set (Var "A"))))))) ; theorem :: SETLIM_1:14 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" ($#v3_funct_1 :::"constant"::: ) ) & (Bool (Set ($#k3_funct_1 :::"the_value_of"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" (Set (Var "B")) ($#k3_funct_2 :::"."::: ) (Set (Var "k")) ")" ) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) "}" ) ($#r1_hidden :::"="::: ) (Set (Var "A"))))))) ; theorem :: SETLIM_1:15 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" (Set (Var "B")) ($#k3_funct_2 :::"."::: ) (Set (Var "k")) ")" ) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) "}" )) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")))))) ; theorem :: SETLIM_1:16 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set (Var "B")) ($#k3_funct_2 :::"."::: ) (Set (Var "k")) ")" ) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) "}" )) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "X")) ")" ))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "B" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "X")); attr "B" is :::"monotone"::: means :: SETLIM_1:def 1 (Bool "(" "not" (Bool "B" "is" bbbadV3_PROB_1()) "or" "not" (Bool "B" "is" bbbadV2_PROB_1()) ")" ); end; :: deftheorem defines :::"monotone"::: SETLIM_1:def 1 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#v1_setlim_1 :::"monotone"::: ) ) "iff" (Bool "(" "not" (Bool (Set (Var "B")) "is" bbbadV3_PROB_1()) "or" "not" (Bool (Set (Var "B")) "is" bbbadV2_PROB_1()) ")" ) ")" ))); definitionlet "B" be ($#m1_hidden :::"Function":::); func :::"inferior_setsequence"::: "B" -> ($#m1_hidden :::"Function":::) means :: SETLIM_1:def 2 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" "B" ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) "}" )) ")" ) ")" ); end; :: deftheorem defines :::"inferior_setsequence"::: SETLIM_1:def 2 : (Bool "for" (Set (Var "B")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "B")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) "{" (Set "(" (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) "}" )) ")" ) ")" ) ")" )); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "B" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "X")); :: original: :::"inferior_setsequence"::: redefine func :::"inferior_setsequence"::: "B" -> ($#m1_subset_1 :::"SetSequence":::) "of" "X"; end; definitionlet "B" be ($#m1_hidden :::"Function":::); func :::"superior_setsequence"::: "B" -> ($#m1_hidden :::"Function":::) means :: SETLIM_1:def 3 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" "B" ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) "}" )) ")" ) ")" ); end; :: deftheorem defines :::"superior_setsequence"::: SETLIM_1:def 3 : (Bool "for" (Set (Var "B")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_setlim_1 :::"superior_setsequence"::: ) (Set (Var "B")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")) ")" ) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) "}" )) ")" ) ")" ) ")" )); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "B" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "X")); :: original: :::"superior_setsequence"::: redefine func :::"superior_setsequence"::: "B" -> ($#m1_subset_1 :::"SetSequence":::) "of" "X"; end; theorem :: SETLIM_1:17 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "B")))))) ; theorem :: SETLIM_1:18 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_kurato_0 :::"Union"::: ) (Set (Var "B")))))) ; theorem :: SETLIM_1:19 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n")))) "iff" (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "B")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" )))) ")" )))) ; theorem :: SETLIM_1:20 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n")))) "iff" (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "B")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" )))) ")" )))) ; theorem :: SETLIM_1:21 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k5_prob_1 :::"/\"::: ) (Set "(" (Set (Var "B")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" )))))) ; theorem :: SETLIM_1:22 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k6_prob_1 :::"\/"::: ) (Set "(" (Set (Var "B")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" )))))) ; theorem :: SETLIM_1:23 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "B"))) "is" bbbadV3_PROB_1()))) ; theorem :: SETLIM_1:24 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "B"))) "is" bbbadV2_PROB_1()))) ; theorem :: SETLIM_1:25 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "B"))) "is" ($#v1_setlim_1 :::"monotone"::: ) ) & (Bool (Set ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "B"))) "is" ($#v1_setlim_1 :::"monotone"::: ) ) ")" ))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "X")); cluster (Set ($#k1_setlim_1 :::"inferior_setsequence"::: ) "A") -> bbbadV3_PROB_1() for ($#m1_subset_1 :::"SetSequence":::) "of" "X"; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "X")); cluster (Set ($#k3_setlim_1 :::"superior_setsequence"::: ) "A") -> bbbadV2_PROB_1() for ($#m1_subset_1 :::"SetSequence":::) "of" "X"; end; theorem :: SETLIM_1:26 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))))))) ; theorem :: SETLIM_1:27 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_kurato_0 :::"Union"::: ) (Set (Var "B"))))))) ; theorem :: SETLIM_1:28 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "{" (Set "(" (Set (Var "B")) ($#k3_funct_2 :::"."::: ) (Set (Var "k")) ")" ) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) "}" "is" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")))))) ; theorem :: SETLIM_1:29 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_kurato_0 :::"Union"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_prob_1 :::"Intersection"::: ) (Set "(" ($#k2_prob_1 :::"Complement"::: ) (Set (Var "B")) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) )))) ; theorem :: SETLIM_1:30 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set "(" ($#k2_prob_1 :::"Complement"::: ) (Set (Var "B")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_subset_1 :::"`"::: ) ))))) ; theorem :: SETLIM_1:31 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set "(" ($#k2_prob_1 :::"Complement"::: ) (Set (Var "B")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_subset_1 :::"`"::: ) ))))) ; theorem :: SETLIM_1:32 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k2_prob_1 :::"Complement"::: ) (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "B")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set "(" ($#k2_prob_1 :::"Complement"::: ) (Set (Var "B")) ")" ))))) ; theorem :: SETLIM_1:33 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k2_prob_1 :::"Complement"::: ) (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "B")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set "(" ($#k2_prob_1 :::"Complement"::: ) (Set (Var "B")) ")" ))))) ; theorem :: SETLIM_1:34 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A3")) "," (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "A3")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A1")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k6_prob_1 :::"\/"::: ) (Set "(" (Set (Var "A2")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "A1")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k6_prob_1 :::"\/"::: ) (Set "(" (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "A2")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "A3")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))))))) ; theorem :: SETLIM_1:35 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A3")) "," (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "A3")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A1")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_prob_1 :::"/\"::: ) (Set "(" (Set (Var "A2")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "A3")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "A1")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_prob_1 :::"/\"::: ) (Set "(" (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "A2")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" )))))) ; theorem :: SETLIM_1:36 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A3")) "," (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "A3")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A1")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k6_prob_1 :::"\/"::: ) (Set "(" (Set (Var "A2")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "A3")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "A1")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k6_prob_1 :::"\/"::: ) (Set "(" (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "A2")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" )))))) ; theorem :: SETLIM_1:37 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A3")) "," (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "A3")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A1")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_prob_1 :::"/\"::: ) (Set "(" (Set (Var "A2")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "A3")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "A1")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_prob_1 :::"/\"::: ) (Set "(" (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "A2")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" )))))) ; theorem :: SETLIM_1:38 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" ($#v3_funct_1 :::"constant"::: ) ) & (Bool (Set ($#k3_funct_1 :::"the_value_of"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))))))) ; theorem :: SETLIM_1:39 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" ($#v3_funct_1 :::"constant"::: ) ) & (Bool (Set ($#k3_funct_1 :::"the_value_of"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))))))) ; theorem :: SETLIM_1:40 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" bbbadV3_PROB_1())) "holds" (Bool (Set (Set (Var "B")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))))) ; theorem :: SETLIM_1:41 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" bbbadV3_PROB_1())) "holds" (Bool (Set (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))))) ; theorem :: SETLIM_1:42 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" bbbadV3_PROB_1())) "holds" (Bool (Set (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_kurato_0 :::"Union"::: ) (Set (Var "B"))))))) ; theorem :: SETLIM_1:43 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" bbbadV3_PROB_1())) "holds" (Bool (Set ($#k3_prob_1 :::"Intersection"::: ) (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_kurato_0 :::"Union"::: ) (Set (Var "B")))))) ; theorem :: SETLIM_1:44 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" bbbadV3_PROB_1())) "holds" (Bool (Set (Set (Var "B")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))))) ; theorem :: SETLIM_1:45 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" bbbadV3_PROB_1())) "holds" (Bool (Set (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))))))) ; theorem :: SETLIM_1:46 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" bbbadV3_PROB_1())) "holds" (Bool (Set ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "B"))) ($#r2_funct_2 :::"="::: ) (Set (Var "B"))))) ; theorem :: SETLIM_1:47 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" bbbadV2_PROB_1())) "holds" (Bool (Set (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))))))) ; theorem :: SETLIM_1:48 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" bbbadV2_PROB_1())) "holds" (Bool (Set (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))))))) ; theorem :: SETLIM_1:49 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" bbbadV2_PROB_1())) "holds" (Bool (Set ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "B"))) ($#r2_funct_2 :::"="::: ) (Set (Var "B"))))) ; theorem :: SETLIM_1:50 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" bbbadV2_PROB_1())) "holds" (Bool (Set (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))))))) ; theorem :: SETLIM_1:51 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" bbbadV2_PROB_1())) "holds" (Bool (Set (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))))) ; theorem :: SETLIM_1:52 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" bbbadV2_PROB_1())) "holds" (Bool (Set (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "B")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "B"))))))) ; theorem :: SETLIM_1:53 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" bbbadV2_PROB_1())) "holds" (Bool (Set ($#k1_kurato_0 :::"Union"::: ) (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "B")))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "B" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "X")); redefine func :::"lim_inf"::: "B" equals :: SETLIM_1:def 4 (Set ($#k1_kurato_0 :::"Union"::: ) (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) "B" ")" )); end; :: deftheorem defines :::"lim_inf"::: SETLIM_1:def 4 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k1_kurato_0 :::"Union"::: ) (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "B")) ")" ))))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "B" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "X")); redefine func :::"lim_sup"::: "B" equals :: SETLIM_1:def 5 (Set ($#k3_prob_1 :::"Intersection"::: ) (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) "B" ")" )); end; :: deftheorem defines :::"lim_sup"::: SETLIM_1:def 5 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k3_prob_1 :::"Intersection"::: ) (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "B")) ")" ))))); notationlet "X" be ($#m1_hidden :::"set"::: ) ; let "B" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "X")); synonym :::"lim"::: "B" for :::"lim_sup"::: "B"; end; theorem :: SETLIM_1:54 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "B")))))) ; theorem :: SETLIM_1:55 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k4_kurato_0 :::"lim"::: ) (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "B")) ")" ))))) ; theorem :: SETLIM_1:56 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k4_kurato_0 :::"lim"::: ) (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "B")) ")" ))))) ; theorem :: SETLIM_1:57 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set "(" ($#k2_prob_1 :::"Complement"::: ) (Set (Var "B")) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) )))) ; theorem :: SETLIM_1:58 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" ($#v3_funct_1 :::"constant"::: ) ) & (Bool (Set ($#k3_funct_1 :::"the_value_of"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#v3_kurato_0 :::"convergent"::: ) ) & (Bool (Set ($#k4_kurato_0 :::"lim"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) ")" )))) ; theorem :: SETLIM_1:59 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" bbbadV3_PROB_1())) "holds" (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k1_kurato_0 :::"Union"::: ) (Set (Var "B")))))) ; theorem :: SETLIM_1:60 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" bbbadV3_PROB_1())) "holds" (Bool (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k1_kurato_0 :::"Union"::: ) (Set (Var "B")))))) ; theorem :: SETLIM_1:61 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" bbbadV2_PROB_1())) "holds" (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "B")))))) ; theorem :: SETLIM_1:62 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" bbbadV2_PROB_1())) "holds" (Bool (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "B")))))) ; theorem :: SETLIM_1:63 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" bbbadV3_PROB_1())) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#v3_kurato_0 :::"convergent"::: ) ) & (Bool (Set ($#k4_kurato_0 :::"lim"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k1_kurato_0 :::"Union"::: ) (Set (Var "B")))) ")" ))) ; theorem :: SETLIM_1:64 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" bbbadV2_PROB_1())) "holds" (Bool "(" (Bool (Set (Var "B")) "is" ($#v3_kurato_0 :::"convergent"::: ) ) & (Bool (Set ($#k4_kurato_0 :::"lim"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "B")))) ")" ))) ; theorem :: SETLIM_1:65 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "B")) "is" ($#v1_setlim_1 :::"monotone"::: ) )) "holds" (Bool (Set (Var "B")) "is" ($#v3_kurato_0 :::"convergent"::: ) ))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Si" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "S" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "Si")); :: original: :::"inferior_setsequence"::: redefine func :::"inferior_setsequence"::: "S" -> ($#m1_subset_1 :::"SetSequence":::) "of" "Si"; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Si" be ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Const "X")); let "S" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "Si")); :: original: :::"superior_setsequence"::: redefine func :::"superior_setsequence"::: "S" -> ($#m1_subset_1 :::"SetSequence":::) "of" "Si"; end; theorem :: SETLIM_1:66 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "S")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "S")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ))))) ")" )))) ; theorem :: SETLIM_1:67 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "S")))) "iff" (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "S")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ))))) ")" )))) ; theorem :: SETLIM_1:68 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "holds" (Bool (Set ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "S"))))))) ; theorem :: SETLIM_1:69 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "holds" (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_kurato_0 :::"Union"::: ) (Set (Var "S"))))))) ; theorem :: SETLIM_1:70 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "holds" (Bool (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "S"))))))) ; theorem :: SETLIM_1:71 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "holds" (Bool (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set "(" ($#k2_prob_1 :::"Complement"::: ) (Set (Var "S")) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) ))))) ; theorem :: SETLIM_1:72 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "holds" (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set "(" ($#k2_prob_1 :::"Complement"::: ) (Set (Var "S")) ")" ) ")" ) ($#k3_subset_1 :::"`"::: ) ))))) ; theorem :: SETLIM_1:73 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S3")) "," (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "S3")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "S1")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k6_prob_1 :::"\/"::: ) (Set "(" (Set (Var "S2")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool (Set (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "S1")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "S2")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "S3"))))))) ; theorem :: SETLIM_1:74 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S3")) "," (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "S3")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "S1")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_prob_1 :::"/\"::: ) (Set "(" (Set (Var "S2")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "S3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "S1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "S2")) ")" )))))) ; theorem :: SETLIM_1:75 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S3")) "," (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "S3")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "S1")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k6_prob_1 :::"\/"::: ) (Set "(" (Set (Var "S2")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "S3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "S1")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "S2")) ")" )))))) ; theorem :: SETLIM_1:76 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S3")) "," (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "S3")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "S1")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_prob_1 :::"/\"::: ) (Set "(" (Set (Var "S2")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "S3"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "S1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "S2")) ")" )))))) ; theorem :: SETLIM_1:77 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v3_funct_1 :::"constant"::: ) ) & (Bool (Set ($#k3_funct_1 :::"the_value_of"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Var "A")))) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_kurato_0 :::"convergent"::: ) ) & (Bool (Set ($#k4_kurato_0 :::"lim"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) ")" ))))) ; theorem :: SETLIM_1:78 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "st" (Bool (Bool (Set (Var "S")) "is" bbbadV3_PROB_1())) "holds" (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k1_kurato_0 :::"Union"::: ) (Set (Var "S"))))))) ; theorem :: SETLIM_1:79 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "st" (Bool (Bool (Set (Var "S")) "is" bbbadV3_PROB_1())) "holds" (Bool (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k1_kurato_0 :::"Union"::: ) (Set (Var "S"))))))) ; theorem :: SETLIM_1:80 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "st" (Bool (Bool (Set (Var "S")) "is" bbbadV3_PROB_1())) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_kurato_0 :::"convergent"::: ) ) & (Bool (Set ($#k4_kurato_0 :::"lim"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k1_kurato_0 :::"Union"::: ) (Set (Var "S")))) ")" )))) ; theorem :: SETLIM_1:81 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "st" (Bool (Bool (Set (Var "S")) "is" bbbadV2_PROB_1())) "holds" (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "S"))))))) ; theorem :: SETLIM_1:82 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "st" (Bool (Bool (Set (Var "S")) "is" bbbadV2_PROB_1())) "holds" (Bool (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "S"))))))) ; theorem :: SETLIM_1:83 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "st" (Bool (Bool (Set (Var "S")) "is" bbbadV2_PROB_1())) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_kurato_0 :::"convergent"::: ) ) & (Bool (Set ($#k4_kurato_0 :::"lim"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "S")))) ")" )))) ; theorem :: SETLIM_1:84 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Si")) "being" ($#m1_subset_1 :::"SigmaField":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "Si")) "st" (Bool (Bool (Set (Var "S")) "is" ($#v1_setlim_1 :::"monotone"::: ) )) "holds" (Bool (Set (Var "S")) "is" ($#v3_kurato_0 :::"convergent"::: ) )))) ;