:: SETLIM_2 semantic presentation begin theorem :: SETLIM_2:1 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "A1")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k3_prob_1 :::"Intersection"::: ) (Set "(" (Set (Var "A1")) ($#k10_nat_1 :::"^\"::: ) (Set (Var "n")) ")" )))))) ; theorem :: SETLIM_2:2 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "A1")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_prob_1 :::"Union"::: ) (Set "(" (Set (Var "A1")) ($#k10_nat_1 :::"^\"::: ) (Set (Var "n")) ")" )))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "A1", "A2" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "X")); func "A1" :::"(/\)"::: "A2" -> ($#m1_subset_1 :::"SetSequence":::) "of" "X" means :: SETLIM_2:def 1 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "A1" ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" "A2" ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )))); commutativity (Bool "for" (Set (Var "b1")) "," (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "X")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A1")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "A2")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A2")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "A1")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))))) ; func "A1" :::"(\/)"::: "A2" -> ($#m1_subset_1 :::"SetSequence":::) "of" "X" means :: SETLIM_2:def 2 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "A1" ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" "A2" ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )))); commutativity (Bool "for" (Set (Var "b1")) "," (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "X")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A1")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "A2")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A2")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "A1")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))))) ; func "A1" :::"(\)"::: "A2" -> ($#m1_subset_1 :::"SetSequence":::) "of" "X" means :: SETLIM_2:def 3 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "A1" ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" "A2" ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )))); func "A1" :::"(\+\)"::: "A2" -> ($#m1_subset_1 :::"SetSequence":::) "of" "X" means :: SETLIM_2:def 4 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "A1" ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_subset_1 :::"\+\"::: ) (Set "(" "A2" ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )))); commutativity (Bool "for" (Set (Var "b1")) "," (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "X")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A1")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_subset_1 :::"\+\"::: ) (Set "(" (Set (Var "A2")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A2")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_subset_1 :::"\+\"::: ) (Set "(" (Set (Var "A1")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))))) ; end; :: deftheorem defines :::"(/\)"::: SETLIM_2:def 1 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k1_setlim_2 :::"(/\)"::: ) (Set (Var "A2")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b4")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A1")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "A2")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )))) ")" ))); :: deftheorem defines :::"(\/)"::: SETLIM_2:def 2 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k2_setlim_2 :::"(\/)"::: ) (Set (Var "A2")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b4")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A1")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "A2")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )))) ")" ))); :: deftheorem defines :::"(\)"::: SETLIM_2:def 3 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k3_setlim_2 :::"(\)"::: ) (Set (Var "A2")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b4")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A1")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set (Var "A2")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )))) ")" ))); :: deftheorem defines :::"(\+\)"::: SETLIM_2:def 4 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k4_setlim_2 :::"(\+\)"::: ) (Set (Var "A2")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b4")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A1")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_subset_1 :::"\+\"::: ) (Set "(" (Set (Var "A2")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )))) ")" ))); theorem :: SETLIM_2:3 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "A1")) ($#k4_setlim_2 :::"(\+\)"::: ) (Set (Var "A2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A1")) ($#k3_setlim_2 :::"(\)"::: ) (Set (Var "A2")) ")" ) ($#k2_setlim_2 :::"(\/)"::: ) (Set "(" (Set (Var "A2")) ($#k3_setlim_2 :::"(\)"::: ) (Set (Var "A1")) ")" ))))) ; theorem :: SETLIM_2:4 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "A1")) ($#k1_setlim_2 :::"(/\)"::: ) (Set (Var "A2")) ")" ) ($#k10_nat_1 :::"^\"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A1")) ($#k10_nat_1 :::"^\"::: ) (Set (Var "k")) ")" ) ($#k1_setlim_2 :::"(/\)"::: ) (Set "(" (Set (Var "A2")) ($#k10_nat_1 :::"^\"::: ) (Set (Var "k")) ")" )))))) ; theorem :: SETLIM_2:5 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "A1")) ($#k2_setlim_2 :::"(\/)"::: ) (Set (Var "A2")) ")" ) ($#k10_nat_1 :::"^\"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A1")) ($#k10_nat_1 :::"^\"::: ) (Set (Var "k")) ")" ) ($#k2_setlim_2 :::"(\/)"::: ) (Set "(" (Set (Var "A2")) ($#k10_nat_1 :::"^\"::: ) (Set (Var "k")) ")" )))))) ; theorem :: SETLIM_2:6 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "A1")) ($#k3_setlim_2 :::"(\)"::: ) (Set (Var "A2")) ")" ) ($#k10_nat_1 :::"^\"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A1")) ($#k10_nat_1 :::"^\"::: ) (Set (Var "k")) ")" ) ($#k3_setlim_2 :::"(\)"::: ) (Set "(" (Set (Var "A2")) ($#k10_nat_1 :::"^\"::: ) (Set (Var "k")) ")" )))))) ; theorem :: SETLIM_2:7 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "A1")) ($#k4_setlim_2 :::"(\+\)"::: ) (Set (Var "A2")) ")" ) ($#k10_nat_1 :::"^\"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A1")) ($#k10_nat_1 :::"^\"::: ) (Set (Var "k")) ")" ) ($#k4_setlim_2 :::"(\+\)"::: ) (Set "(" (Set (Var "A2")) ($#k10_nat_1 :::"^\"::: ) (Set (Var "k")) ")" )))))) ; theorem :: SETLIM_2:8 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_prob_1 :::"Union"::: ) (Set "(" (Set (Var "A1")) ($#k1_setlim_2 :::"(/\)"::: ) (Set (Var "A2")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_prob_1 :::"Union"::: ) (Set (Var "A1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_prob_1 :::"Union"::: ) (Set (Var "A2")) ")" ))))) ; theorem :: SETLIM_2:9 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_prob_1 :::"Union"::: ) (Set "(" (Set (Var "A1")) ($#k2_setlim_2 :::"(\/)"::: ) (Set (Var "A2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_prob_1 :::"Union"::: ) (Set (Var "A1")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_prob_1 :::"Union"::: ) (Set (Var "A2")) ")" ))))) ; theorem :: SETLIM_2:10 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k1_prob_1 :::"Union"::: ) (Set (Var "A1")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k1_prob_1 :::"Union"::: ) (Set (Var "A2")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k1_prob_1 :::"Union"::: ) (Set "(" (Set (Var "A1")) ($#k3_setlim_2 :::"(\)"::: ) (Set (Var "A2")) ")" ))))) ; theorem :: SETLIM_2:11 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k1_prob_1 :::"Union"::: ) (Set (Var "A1")) ")" ) ($#k5_subset_1 :::"\+\"::: ) (Set "(" ($#k1_prob_1 :::"Union"::: ) (Set (Var "A2")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k1_prob_1 :::"Union"::: ) (Set "(" (Set (Var "A1")) ($#k4_setlim_2 :::"(\+\)"::: ) (Set (Var "A2")) ")" ))))) ; theorem :: SETLIM_2:12 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_prob_1 :::"Intersection"::: ) (Set "(" (Set (Var "A1")) ($#k1_setlim_2 :::"(/\)"::: ) (Set (Var "A2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "A1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "A2")) ")" ))))) ; theorem :: SETLIM_2:13 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "A1")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "A2")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k3_prob_1 :::"Intersection"::: ) (Set "(" (Set (Var "A1")) ($#k2_setlim_2 :::"(\/)"::: ) (Set (Var "A2")) ")" ))))) ; theorem :: SETLIM_2:14 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_prob_1 :::"Intersection"::: ) (Set "(" (Set (Var "A1")) ($#k3_setlim_2 :::"(\)"::: ) (Set (Var "A2")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "A1")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "A2")) ")" ))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "A1" be ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Const "X")); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); func "A" :::"(/\)"::: "A1" -> ($#m1_subset_1 :::"SetSequence":::) "of" "X" means :: SETLIM_2:def 5 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set "A" ($#k9_subset_1 :::"/\"::: ) (Set "(" "A1" ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )))); func "A" :::"(\/)"::: "A1" -> ($#m1_subset_1 :::"SetSequence":::) "of" "X" means :: SETLIM_2:def 6 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set "A" ($#k4_subset_1 :::"\/"::: ) (Set "(" "A1" ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )))); func "A" :::"(\)"::: "A1" -> ($#m1_subset_1 :::"SetSequence":::) "of" "X" means :: SETLIM_2:def 7 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set "A" ($#k7_subset_1 :::"\"::: ) (Set "(" "A1" ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )))); func "A1" :::"(\)"::: "A" -> ($#m1_subset_1 :::"SetSequence":::) "of" "X" means :: SETLIM_2:def 8 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "A1" ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k7_subset_1 :::"\"::: ) "A"))); func "A" :::"(\+\)"::: "A1" -> ($#m1_subset_1 :::"SetSequence":::) "of" "X" means :: SETLIM_2:def 9 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set "A" ($#k5_subset_1 :::"\+\"::: ) (Set "(" "A1" ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )))); end; :: deftheorem defines :::"(/\)"::: SETLIM_2:def 5 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k5_setlim_2 :::"(/\)"::: ) (Set (Var "A1")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b4")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "A1")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )))) ")" ))))); :: deftheorem defines :::"(\/)"::: SETLIM_2:def 6 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k6_setlim_2 :::"(\/)"::: ) (Set (Var "A1")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b4")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "A1")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )))) ")" ))))); :: deftheorem defines :::"(\)"::: SETLIM_2:def 7 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k7_setlim_2 :::"(\)"::: ) (Set (Var "A1")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b4")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set (Var "A1")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )))) ")" ))))); :: deftheorem defines :::"(\)"::: SETLIM_2:def 8 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A1")) ($#k8_setlim_2 :::"(\)"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b4")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A1")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A"))))) ")" ))))); :: deftheorem defines :::"(\+\)"::: SETLIM_2:def 9 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k9_setlim_2 :::"(\+\)"::: ) (Set (Var "A1")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b4")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k5_subset_1 :::"\+\"::: ) (Set "(" (Set (Var "A1")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )))) ")" ))))); theorem :: SETLIM_2:15 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "A")) ($#k9_setlim_2 :::"(\+\)"::: ) (Set (Var "A1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k7_setlim_2 :::"(\)"::: ) (Set (Var "A1")) ")" ) ($#k2_setlim_2 :::"(\/)"::: ) (Set "(" (Set (Var "A1")) ($#k8_setlim_2 :::"(\)"::: ) (Set (Var "A")) ")" )))))) ; theorem :: SETLIM_2:16 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k5_setlim_2 :::"(/\)"::: ) (Set (Var "A1")) ")" ) ($#k10_nat_1 :::"^\"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k5_setlim_2 :::"(/\)"::: ) (Set "(" (Set (Var "A1")) ($#k10_nat_1 :::"^\"::: ) (Set (Var "k")) ")" ))))))) ; theorem :: SETLIM_2:17 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k6_setlim_2 :::"(\/)"::: ) (Set (Var "A1")) ")" ) ($#k10_nat_1 :::"^\"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k6_setlim_2 :::"(\/)"::: ) (Set "(" (Set (Var "A1")) ($#k10_nat_1 :::"^\"::: ) (Set (Var "k")) ")" ))))))) ; theorem :: SETLIM_2:18 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k7_setlim_2 :::"(\)"::: ) (Set (Var "A1")) ")" ) ($#k10_nat_1 :::"^\"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k7_setlim_2 :::"(\)"::: ) (Set "(" (Set (Var "A1")) ($#k10_nat_1 :::"^\"::: ) (Set (Var "k")) ")" ))))))) ; theorem :: SETLIM_2:19 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "A1")) ($#k8_setlim_2 :::"(\)"::: ) (Set (Var "A")) ")" ) ($#k10_nat_1 :::"^\"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A1")) ($#k10_nat_1 :::"^\"::: ) (Set (Var "k")) ")" ) ($#k8_setlim_2 :::"(\)"::: ) (Set (Var "A")))))))) ; theorem :: SETLIM_2:20 (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k9_setlim_2 :::"(\+\)"::: ) (Set (Var "A1")) ")" ) ($#k10_nat_1 :::"^\"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k9_setlim_2 :::"(\+\)"::: ) (Set "(" (Set (Var "A1")) ($#k10_nat_1 :::"^\"::: ) (Set (Var "k")) ")" ))))))) ; theorem :: SETLIM_2:21 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v2_prob_1 :::"non-ascending"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k5_setlim_2 :::"(/\)"::: ) (Set (Var "A1"))) "is" ($#v2_prob_1 :::"non-ascending"::: ) )))) ; theorem :: SETLIM_2:22 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v3_prob_1 :::"non-descending"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k5_setlim_2 :::"(/\)"::: ) (Set (Var "A1"))) "is" ($#v3_prob_1 :::"non-descending"::: ) )))) ; theorem :: SETLIM_2:23 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v1_setlim_1 :::"monotone"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k5_setlim_2 :::"(/\)"::: ) (Set (Var "A1"))) "is" ($#v1_setlim_1 :::"monotone"::: ) )))) ; theorem :: SETLIM_2:24 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v2_prob_1 :::"non-ascending"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k6_setlim_2 :::"(\/)"::: ) (Set (Var "A1"))) "is" ($#v2_prob_1 :::"non-ascending"::: ) )))) ; theorem :: SETLIM_2:25 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v3_prob_1 :::"non-descending"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k6_setlim_2 :::"(\/)"::: ) (Set (Var "A1"))) "is" ($#v3_prob_1 :::"non-descending"::: ) )))) ; theorem :: SETLIM_2:26 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v1_setlim_1 :::"monotone"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k6_setlim_2 :::"(\/)"::: ) (Set (Var "A1"))) "is" ($#v1_setlim_1 :::"monotone"::: ) )))) ; theorem :: SETLIM_2:27 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v2_prob_1 :::"non-ascending"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k7_setlim_2 :::"(\)"::: ) (Set (Var "A1"))) "is" ($#v3_prob_1 :::"non-descending"::: ) )))) ; theorem :: SETLIM_2:28 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v3_prob_1 :::"non-descending"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k7_setlim_2 :::"(\)"::: ) (Set (Var "A1"))) "is" ($#v2_prob_1 :::"non-ascending"::: ) )))) ; theorem :: SETLIM_2:29 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v1_setlim_1 :::"monotone"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k7_setlim_2 :::"(\)"::: ) (Set (Var "A1"))) "is" ($#v1_setlim_1 :::"monotone"::: ) )))) ; theorem :: SETLIM_2:30 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v2_prob_1 :::"non-ascending"::: ) )) "holds" (Bool (Set (Set (Var "A1")) ($#k8_setlim_2 :::"(\)"::: ) (Set (Var "A"))) "is" ($#v2_prob_1 :::"non-ascending"::: ) )))) ; theorem :: SETLIM_2:31 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v3_prob_1 :::"non-descending"::: ) )) "holds" (Bool (Set (Set (Var "A1")) ($#k8_setlim_2 :::"(\)"::: ) (Set (Var "A"))) "is" ($#v3_prob_1 :::"non-descending"::: ) )))) ; theorem :: SETLIM_2:32 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v1_setlim_1 :::"monotone"::: ) )) "holds" (Bool (Set (Set (Var "A1")) ($#k8_setlim_2 :::"(\)"::: ) (Set (Var "A"))) "is" ($#v1_setlim_1 :::"monotone"::: ) )))) ; theorem :: SETLIM_2:33 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_prob_1 :::"Intersection"::: ) (Set "(" (Set (Var "A")) ($#k5_setlim_2 :::"(/\)"::: ) (Set (Var "A1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "A1")) ")" )))))) ; theorem :: SETLIM_2:34 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_prob_1 :::"Intersection"::: ) (Set "(" (Set (Var "A")) ($#k6_setlim_2 :::"(\/)"::: ) (Set (Var "A1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "A1")) ")" )))))) ; theorem :: SETLIM_2:35 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_prob_1 :::"Intersection"::: ) (Set "(" (Set (Var "A")) ($#k7_setlim_2 :::"(\)"::: ) (Set (Var "A1")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "A1")) ")" )))))) ; theorem :: SETLIM_2:36 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_prob_1 :::"Intersection"::: ) (Set "(" (Set (Var "A1")) ($#k8_setlim_2 :::"(\)"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "A1")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A"))))))) ; theorem :: SETLIM_2:37 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_prob_1 :::"Intersection"::: ) (Set "(" (Set (Var "A")) ($#k9_setlim_2 :::"(\+\)"::: ) (Set (Var "A1")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k5_subset_1 :::"\+\"::: ) (Set "(" ($#k3_prob_1 :::"Intersection"::: ) (Set (Var "A1")) ")" )))))) ; theorem :: SETLIM_2: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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_prob_1 :::"Union"::: ) (Set "(" (Set (Var "A")) ($#k5_setlim_2 :::"(/\)"::: ) (Set (Var "A1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_prob_1 :::"Union"::: ) (Set (Var "A1")) ")" )))))) ; theorem :: SETLIM_2: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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_prob_1 :::"Union"::: ) (Set "(" (Set (Var "A")) ($#k6_setlim_2 :::"(\/)"::: ) (Set (Var "A1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k1_prob_1 :::"Union"::: ) (Set (Var "A1")) ")" )))))) ; theorem :: SETLIM_2:40 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k1_prob_1 :::"Union"::: ) (Set (Var "A1")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k1_prob_1 :::"Union"::: ) (Set "(" (Set (Var "A")) ($#k7_setlim_2 :::"(\)"::: ) (Set (Var "A1")) ")" )))))) ; theorem :: SETLIM_2:41 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_prob_1 :::"Union"::: ) (Set "(" (Set (Var "A1")) ($#k8_setlim_2 :::"(\)"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_prob_1 :::"Union"::: ) (Set (Var "A1")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A"))))))) ; theorem :: SETLIM_2:42 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "A")) ($#k5_subset_1 :::"\+\"::: ) (Set "(" ($#k1_prob_1 :::"Union"::: ) (Set (Var "A1")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k1_prob_1 :::"Union"::: ) (Set "(" (Set (Var "A")) ($#k9_setlim_2 :::"(\+\)"::: ) (Set (Var "A1")) ")" )))))) ; theorem :: SETLIM_2:43 (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 "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set "(" (Set (Var "A1")) ($#k1_setlim_2 :::"(/\)"::: ) (Set (Var "A2")) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "A1")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "A2")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )))))) ; theorem :: SETLIM_2: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 "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "A1")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "A2")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set "(" (Set (Var "A1")) ($#k2_setlim_2 :::"(\/)"::: ) (Set (Var "A2")) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))))))) ; theorem :: SETLIM_2: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 "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set "(" (Set (Var "A1")) ($#k3_setlim_2 :::"(\)"::: ) (Set (Var "A2")) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "A1")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "A2")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )))))) ; theorem :: SETLIM_2:46 (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 "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set "(" (Set (Var "A1")) ($#k1_setlim_2 :::"(/\)"::: ) (Set (Var "A2")) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "A1")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "A2")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )))))) ; theorem :: SETLIM_2: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 "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set "(" (Set (Var "A1")) ($#k2_setlim_2 :::"(\/)"::: ) (Set (Var "A2")) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "A1")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "A2")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )))))) ; theorem :: SETLIM_2: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 "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "A1")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "A2")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set "(" (Set (Var "A1")) ($#k3_setlim_2 :::"(\)"::: ) (Set (Var "A2")) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))))))) ; theorem :: SETLIM_2:49 (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 "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "A1")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_subset_1 :::"\+\"::: ) (Set "(" (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "A2")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set "(" (Set (Var "A1")) ($#k4_setlim_2 :::"(\+\)"::: ) (Set (Var "A2")) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))))))) ; theorem :: SETLIM_2: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 "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set "(" (Set (Var "A")) ($#k5_setlim_2 :::"(/\)"::: ) (Set (Var "A1")) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "A1")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))))))) ; theorem :: SETLIM_2: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 "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set "(" (Set (Var "A")) ($#k6_setlim_2 :::"(\/)"::: ) (Set (Var "A1")) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "A1")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))))))) ; theorem :: SETLIM_2: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 "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set "(" (Set (Var "A")) ($#k7_setlim_2 :::"(\)"::: ) (Set (Var "A1")) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "A1")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))))))) ; theorem :: SETLIM_2:53 (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 "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set "(" (Set (Var "A1")) ($#k8_setlim_2 :::"(\)"::: ) (Set (Var "A")) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "A1")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A")))))))) ; theorem :: SETLIM_2:54 (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 "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set "(" (Set (Var "A")) ($#k9_setlim_2 :::"(\+\)"::: ) (Set (Var "A1")) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k5_subset_1 :::"\+\"::: ) (Set "(" (Set "(" ($#k2_setlim_1 :::"inferior_setsequence"::: ) (Set (Var "A1")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))))))) ; theorem :: SETLIM_2:55 (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 "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set "(" (Set (Var "A")) ($#k5_setlim_2 :::"(/\)"::: ) (Set (Var "A1")) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "A1")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))))))) ; theorem :: SETLIM_2:56 (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 "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set "(" (Set (Var "A")) ($#k6_setlim_2 :::"(\/)"::: ) (Set (Var "A1")) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "A1")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ))))))) ; theorem :: SETLIM_2:57 (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 "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "A1")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set "(" (Set (Var "A")) ($#k7_setlim_2 :::"(\)"::: ) (Set (Var "A1")) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))))))) ; theorem :: SETLIM_2:58 (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 "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set "(" (Set (Var "A1")) ($#k8_setlim_2 :::"(\)"::: ) (Set (Var "A")) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "A1")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A")))))))) ; theorem :: SETLIM_2:59 (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 "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "A")) ($#k5_subset_1 :::"\+\"::: ) (Set "(" (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set (Var "A1")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k4_setlim_1 :::"superior_setsequence"::: ) (Set "(" (Set (Var "A")) ($#k9_setlim_2 :::"(\+\)"::: ) (Set (Var "A1")) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))))))) ; theorem :: SETLIM_2:60 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set "(" (Set (Var "A1")) ($#k1_setlim_2 :::"(/\)"::: ) (Set (Var "A2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "A1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "A2")) ")" ))))) ; theorem :: SETLIM_2:61 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "A1")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "A2")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set "(" (Set (Var "A1")) ($#k2_setlim_2 :::"(\/)"::: ) (Set (Var "A2")) ")" ))))) ; theorem :: SETLIM_2:62 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set "(" (Set (Var "A1")) ($#k3_setlim_2 :::"(\)"::: ) (Set (Var "A2")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "A1")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "A2")) ")" ))))) ; theorem :: SETLIM_2:63 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" (Bool (Set (Var "A1")) "is" ($#v3_kurato_0 :::"convergent"::: ) ) "or" (Bool (Set (Var "A2")) "is" ($#v3_kurato_0 :::"convergent"::: ) ) ")" )) "holds" (Bool (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set "(" (Set (Var "A1")) ($#k2_setlim_2 :::"(\/)"::: ) (Set (Var "A2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "A1")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "A2")) ")" ))))) ; theorem :: SETLIM_2:64 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A2")) "," (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A2")) "is" ($#v3_kurato_0 :::"convergent"::: ) )) "holds" (Bool (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set "(" (Set (Var "A1")) ($#k3_setlim_2 :::"(\)"::: ) (Set (Var "A2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "A1")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "A2")) ")" ))))) ; theorem :: SETLIM_2:65 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" (Bool (Set (Var "A1")) "is" ($#v3_kurato_0 :::"convergent"::: ) ) "or" (Bool (Set (Var "A2")) "is" ($#v3_kurato_0 :::"convergent"::: ) ) ")" )) "holds" (Bool (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set "(" (Set (Var "A1")) ($#k4_setlim_2 :::"(\+\)"::: ) (Set (Var "A2")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "A1")) ")" ) ($#k5_subset_1 :::"\+\"::: ) (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "A2")) ")" ))))) ; theorem :: SETLIM_2:66 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v3_kurato_0 :::"convergent"::: ) ) & (Bool (Set (Var "A2")) "is" ($#v3_kurato_0 :::"convergent"::: ) )) "holds" (Bool (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set "(" (Set (Var "A1")) ($#k4_setlim_2 :::"(\+\)"::: ) (Set (Var "A2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "A1")) ")" ) ($#k5_subset_1 :::"\+\"::: ) (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "A2")) ")" ))))) ; theorem :: SETLIM_2:67 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set "(" (Set (Var "A1")) ($#k1_setlim_2 :::"(/\)"::: ) (Set (Var "A2")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A2")) ")" ))))) ; theorem :: SETLIM_2:68 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set "(" (Set (Var "A1")) ($#k2_setlim_2 :::"(\/)"::: ) (Set (Var "A2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A1")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A2")) ")" ))))) ; theorem :: SETLIM_2:69 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A1")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A2")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set "(" (Set (Var "A1")) ($#k3_setlim_2 :::"(\)"::: ) (Set (Var "A2")) ")" ))))) ; theorem :: SETLIM_2:70 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A1")) ")" ) ($#k5_subset_1 :::"\+\"::: ) (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A2")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set "(" (Set (Var "A1")) ($#k4_setlim_2 :::"(\+\)"::: ) (Set (Var "A2")) ")" ))))) ; theorem :: SETLIM_2:71 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" (Bool (Set (Var "A1")) "is" ($#v3_kurato_0 :::"convergent"::: ) ) "or" (Bool (Set (Var "A2")) "is" ($#v3_kurato_0 :::"convergent"::: ) ) ")" )) "holds" (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set "(" (Set (Var "A1")) ($#k1_setlim_2 :::"(/\)"::: ) (Set (Var "A2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A2")) ")" ))))) ; theorem :: SETLIM_2:72 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A2")) "," (Set (Var "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A2")) "is" ($#v3_kurato_0 :::"convergent"::: ) )) "holds" (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set "(" (Set (Var "A1")) ($#k3_setlim_2 :::"(\)"::: ) (Set (Var "A2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A1")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A2")) ")" ))))) ; theorem :: SETLIM_2:73 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v3_kurato_0 :::"convergent"::: ) ) & (Bool (Set (Var "A2")) "is" ($#v3_kurato_0 :::"convergent"::: ) )) "holds" (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set "(" (Set (Var "A1")) ($#k4_setlim_2 :::"(\+\)"::: ) (Set (Var "A2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A1")) ")" ) ($#k5_subset_1 :::"\+\"::: ) (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A2")) ")" ))))) ; theorem :: SETLIM_2:74 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set "(" (Set (Var "A")) ($#k5_setlim_2 :::"(/\)"::: ) (Set (Var "A1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "A1")) ")" )))))) ; theorem :: SETLIM_2:75 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set "(" (Set (Var "A")) ($#k6_setlim_2 :::"(\/)"::: ) (Set (Var "A1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "A1")) ")" )))))) ; theorem :: SETLIM_2:76 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set "(" (Set (Var "A")) ($#k7_setlim_2 :::"(\)"::: ) (Set (Var "A1")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "A1")) ")" )))))) ; theorem :: SETLIM_2: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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set "(" (Set (Var "A1")) ($#k8_setlim_2 :::"(\)"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "A1")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A"))))))) ; theorem :: SETLIM_2:78 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set "(" (Set (Var "A")) ($#k9_setlim_2 :::"(\+\)"::: ) (Set (Var "A1")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k5_subset_1 :::"\+\"::: ) (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "A1")) ")" )))))) ; theorem :: SETLIM_2:79 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v3_kurato_0 :::"convergent"::: ) )) "holds" (Bool (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set "(" (Set (Var "A")) ($#k7_setlim_2 :::"(\)"::: ) (Set (Var "A1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "A1")) ")" )))))) ; theorem :: SETLIM_2:80 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v3_kurato_0 :::"convergent"::: ) )) "holds" (Bool (Set ($#k3_kurato_0 :::"lim_inf"::: ) (Set "(" (Set (Var "A")) ($#k9_setlim_2 :::"(\+\)"::: ) (Set (Var "A1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k5_subset_1 :::"\+\"::: ) (Set "(" ($#k3_kurato_0 :::"lim_inf"::: ) (Set (Var "A1")) ")" )))))) ; theorem :: SETLIM_2:81 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set "(" (Set (Var "A")) ($#k5_setlim_2 :::"(/\)"::: ) (Set (Var "A1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A1")) ")" )))))) ; theorem :: SETLIM_2:82 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set "(" (Set (Var "A")) ($#k6_setlim_2 :::"(\/)"::: ) (Set (Var "A1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A1")) ")" )))))) ; theorem :: SETLIM_2:83 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A1")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set "(" (Set (Var "A")) ($#k7_setlim_2 :::"(\)"::: ) (Set (Var "A1")) ")" )))))) ; theorem :: SETLIM_2:84 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set "(" (Set (Var "A1")) ($#k8_setlim_2 :::"(\)"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A1")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A"))))))) ; theorem :: SETLIM_2:85 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "A")) ($#k5_subset_1 :::"\+\"::: ) (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A1")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set "(" (Set (Var "A")) ($#k9_setlim_2 :::"(\+\)"::: ) (Set (Var "A1")) ")" )))))) ; theorem :: SETLIM_2:86 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v3_kurato_0 :::"convergent"::: ) )) "holds" (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set "(" (Set (Var "A")) ($#k7_setlim_2 :::"(\)"::: ) (Set (Var "A1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A1")) ")" )))))) ; theorem :: SETLIM_2:87 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v3_kurato_0 :::"convergent"::: ) )) "holds" (Bool (Set ($#k4_kurato_0 :::"lim_sup"::: ) (Set "(" (Set (Var "A")) ($#k9_setlim_2 :::"(\+\)"::: ) (Set (Var "A1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k5_subset_1 :::"\+\"::: ) (Set "(" ($#k4_kurato_0 :::"lim_sup"::: ) (Set (Var "A1")) ")" )))))) ; theorem :: SETLIM_2:88 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v3_kurato_0 :::"convergent"::: ) ) & (Bool (Set (Var "A2")) "is" ($#v3_kurato_0 :::"convergent"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "A1")) ($#k1_setlim_2 :::"(/\)"::: ) (Set (Var "A2"))) "is" ($#v3_kurato_0 :::"convergent"::: ) ) & (Bool (Set ($#k4_kurato_0 :::"lim"::: ) (Set "(" (Set (Var "A1")) ($#k1_setlim_2 :::"(/\)"::: ) (Set (Var "A2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_kurato_0 :::"lim"::: ) (Set (Var "A1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k4_kurato_0 :::"lim"::: ) (Set (Var "A2")) ")" ))) ")" ))) ; theorem :: SETLIM_2:89 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v3_kurato_0 :::"convergent"::: ) ) & (Bool (Set (Var "A2")) "is" ($#v3_kurato_0 :::"convergent"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "A1")) ($#k2_setlim_2 :::"(\/)"::: ) (Set (Var "A2"))) "is" ($#v3_kurato_0 :::"convergent"::: ) ) & (Bool (Set ($#k4_kurato_0 :::"lim"::: ) (Set "(" (Set (Var "A1")) ($#k2_setlim_2 :::"(\/)"::: ) (Set (Var "A2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_kurato_0 :::"lim"::: ) (Set (Var "A1")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k4_kurato_0 :::"lim"::: ) (Set (Var "A2")) ")" ))) ")" ))) ; theorem :: SETLIM_2:90 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v3_kurato_0 :::"convergent"::: ) ) & (Bool (Set (Var "A2")) "is" ($#v3_kurato_0 :::"convergent"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "A1")) ($#k3_setlim_2 :::"(\)"::: ) (Set (Var "A2"))) "is" ($#v3_kurato_0 :::"convergent"::: ) ) & (Bool (Set ($#k4_kurato_0 :::"lim"::: ) (Set "(" (Set (Var "A1")) ($#k3_setlim_2 :::"(\)"::: ) (Set (Var "A2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_kurato_0 :::"lim"::: ) (Set (Var "A1")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k4_kurato_0 :::"lim"::: ) (Set (Var "A2")) ")" ))) ")" ))) ; theorem :: SETLIM_2:91 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v3_kurato_0 :::"convergent"::: ) ) & (Bool (Set (Var "A2")) "is" ($#v3_kurato_0 :::"convergent"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "A1")) ($#k4_setlim_2 :::"(\+\)"::: ) (Set (Var "A2"))) "is" ($#v3_kurato_0 :::"convergent"::: ) ) & (Bool (Set ($#k4_kurato_0 :::"lim"::: ) (Set "(" (Set (Var "A1")) ($#k4_setlim_2 :::"(\+\)"::: ) (Set (Var "A2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_kurato_0 :::"lim"::: ) (Set (Var "A1")) ")" ) ($#k5_subset_1 :::"\+\"::: ) (Set "(" ($#k4_kurato_0 :::"lim"::: ) (Set (Var "A2")) ")" ))) ")" ))) ; theorem :: SETLIM_2:92 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v3_kurato_0 :::"convergent"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k5_setlim_2 :::"(/\)"::: ) (Set (Var "A1"))) "is" ($#v3_kurato_0 :::"convergent"::: ) ) & (Bool (Set ($#k4_kurato_0 :::"lim"::: ) (Set "(" (Set (Var "A")) ($#k5_setlim_2 :::"(/\)"::: ) (Set (Var "A1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k4_kurato_0 :::"lim"::: ) (Set (Var "A1")) ")" ))) ")" )))) ; theorem :: SETLIM_2:93 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v3_kurato_0 :::"convergent"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k6_setlim_2 :::"(\/)"::: ) (Set (Var "A1"))) "is" ($#v3_kurato_0 :::"convergent"::: ) ) & (Bool (Set ($#k4_kurato_0 :::"lim"::: ) (Set "(" (Set (Var "A")) ($#k6_setlim_2 :::"(\/)"::: ) (Set (Var "A1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k4_kurato_0 :::"lim"::: ) (Set (Var "A1")) ")" ))) ")" )))) ; theorem :: SETLIM_2:94 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v3_kurato_0 :::"convergent"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k7_setlim_2 :::"(\)"::: ) (Set (Var "A1"))) "is" ($#v3_kurato_0 :::"convergent"::: ) ) & (Bool (Set ($#k4_kurato_0 :::"lim"::: ) (Set "(" (Set (Var "A")) ($#k7_setlim_2 :::"(\)"::: ) (Set (Var "A1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k4_kurato_0 :::"lim"::: ) (Set (Var "A1")) ")" ))) ")" )))) ; theorem :: SETLIM_2:95 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v3_kurato_0 :::"convergent"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "A1")) ($#k8_setlim_2 :::"(\)"::: ) (Set (Var "A"))) "is" ($#v3_kurato_0 :::"convergent"::: ) ) & (Bool (Set ($#k4_kurato_0 :::"lim"::: ) (Set "(" (Set (Var "A1")) ($#k8_setlim_2 :::"(\)"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_kurato_0 :::"lim"::: ) (Set (Var "A1")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set (Var "A")))) ")" )))) ; theorem :: SETLIM_2:96 (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 "A1")) "being" ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A1")) "is" ($#v3_kurato_0 :::"convergent"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k9_setlim_2 :::"(\+\)"::: ) (Set (Var "A1"))) "is" ($#v3_kurato_0 :::"convergent"::: ) ) & (Bool (Set ($#k4_kurato_0 :::"lim"::: ) (Set "(" (Set (Var "A")) ($#k9_setlim_2 :::"(\+\)"::: ) (Set (Var "A1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k5_subset_1 :::"\+\"::: ) (Set "(" ($#k4_kurato_0 :::"lim"::: ) (Set (Var "A1")) ")" ))) ")" )))) ;