:: FLANG_3 semantic presentation begin theorem :: FLANG_3:1 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) )) & (Bool (Set (Set (Var "B")) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) )) ")" ))) ; begin definitionlet "E" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ); let "n" be ($#m1_hidden :::"Nat":::); func "A" :::"|^.."::: "n" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "E" ($#k8_afinsq_1 :::"^omega"::: ) ")" ) equals :: FLANG_3:def 1 (Set ($#k3_tarski :::"union"::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "E" ($#k8_afinsq_1 :::"^omega"::: ) ")" ) : (Bool "ex" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool "n" ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set "A" ($#k7_flang_1 :::"|^"::: ) (Set (Var "m")))) ")" )) "}" ); end; :: deftheorem defines :::"|^.."::: FLANG_3:def 1 : (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) : (Bool "ex" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "m")))) ")" )) "}" ))))); theorem :: FLANG_3:2 (Bool "for" (Set (Var "E")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n")))) "iff" (Bool "ex" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "m")))) ")" )) ")" )))) ; theorem :: FLANG_3:3 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "m"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n"))))))) ; theorem :: FLANG_3:4 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "iff" (Bool "(" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" )))) ; theorem :: FLANG_3:5 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "m"))))))) ; theorem :: FLANG_3:6 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "k")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set (Set (Var "A")) ($#k1_flang_2 :::"|^"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k"))))))) ; theorem :: FLANG_3:7 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)))) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k1_flang_2 :::"|^"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "m"))))))) ; theorem :: FLANG_3:8 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n"))))))) ; theorem :: FLANG_3:9 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ))))) ; theorem :: FLANG_3:10 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n")))) "iff" (Bool "(" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) ")" )))) ; theorem :: FLANG_3:11 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) )) "iff" (Bool "(" (Bool (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "or" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" )))) ; theorem :: FLANG_3:12 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k1_flang_2 :::"|^"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ")" )))))) ; theorem :: FLANG_3:13 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n"))))))) ; theorem :: FLANG_3:14 (Bool "for" (Set (Var "x")) "," (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))))) "holds" (Bool (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n"))) ($#r1_hidden :::"<>"::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) ))))) ; theorem :: FLANG_3:15 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) "iff" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) "or" (Bool "(" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ) ")" )))) ; theorem :: FLANG_3:16 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n")) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A"))))))) ; theorem :: FLANG_3:17 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "m")) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "m"))))))) ; theorem :: FLANG_3:18 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "m")) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set "(" (Set (Var "m")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n")) ")" )))))) ; theorem :: FLANG_3:19 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "m")) ")" ) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set "(" (Set (Var "m")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")) ")" )))))) ; theorem :: FLANG_3:20 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n")) ")" ) ($#k8_flang_1 :::"*"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n")) ")" ) ($#k2_flang_2 :::"?"::: ) ))))) ; theorem :: FLANG_3:21 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "C")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "m")))) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "C")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "C")) ($#k1_flang_3 :::"|^.."::: ) (Set "(" (Set (Var "m")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n")) ")" )))))) ; theorem :: FLANG_3:22 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n")) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "k")) ")" )))))) ; theorem :: FLANG_3:23 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n")) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A"))))))) ; theorem :: FLANG_3:24 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "k")) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n")) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "k")) ")" )))))) ; theorem :: FLANG_3:25 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "k")) "," (Set (Var "l")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k1_flang_2 :::"|^"::: ) "(" (Set (Var "k")) "," (Set (Var "l")) ")" ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n")) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k1_flang_2 :::"|^"::: ) "(" (Set (Var "k")) "," (Set (Var "l")) ")" ")" )))))) ; theorem :: FLANG_3:26 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "B")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "B")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n")) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A")))) ")" )))) ; theorem :: FLANG_3:27 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "m")) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n")) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "m")) ")" )))))) ; theorem :: FLANG_3:28 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k")))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k"))))))) ; theorem :: FLANG_3:29 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k")))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k"))))))) ; theorem :: FLANG_3:30 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Num 1))))) ; theorem :: FLANG_3:31 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k"))))))) ; theorem :: FLANG_3:32 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "m")) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "m")) ")" )))))) ; theorem :: FLANG_3:33 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "k")) "," (Set (Var "l")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "l")))) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n")) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k1_flang_2 :::"|^"::: ) "(" (Set (Var "k")) "," (Set (Var "l")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "k")) ")" )))))) ; theorem :: FLANG_3:34 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "k")) "," (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "l")))) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k1_flang_2 :::"|^"::: ) "(" (Set (Var "k")) "," (Set (Var "l")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k"))))))) ; theorem :: FLANG_3:35 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "m")) ")" ) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set "(" (Set (Var "m")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")) ")" )))))) ; theorem :: FLANG_3:36 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "m")) ")" ) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n")) ")" ) ($#k7_flang_1 :::"|^"::: ) (Set (Var "m"))))))) ; theorem :: FLANG_3:37 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "C")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "m")))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "C")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "a")) ($#k1_flang_1 :::"^"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "C")) ($#k1_flang_3 :::"|^.."::: ) (Set "(" (Set (Var "m")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n")) ")" ))))))) ; theorem :: FLANG_3:38 (Bool "for" (Set (Var "x")) "," (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))))))) ; theorem :: FLANG_3:39 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k8_flang_1 :::"*"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k8_flang_1 :::"*"::: ) ))))) ; theorem :: FLANG_3:40 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k2_flang_2 :::"?"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k")))) "iff" (Bool "(" (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ) ")" )))) ; theorem :: FLANG_3:41 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k")) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k2_flang_2 :::"?"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k"))))))) ; theorem :: FLANG_3:42 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k")) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k2_flang_2 :::"?"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k2_flang_2 :::"?"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k")) ")" )))))) ; theorem :: FLANG_3:43 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k")) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k")))) & (Bool (Set (Set (Var "B")) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k")))) ")" )))) ; theorem :: FLANG_3:44 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" ) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "B")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k")) ")" )))))) ; theorem :: FLANG_3:45 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "B")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" ) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k"))))))) ; theorem :: FLANG_3:46 (Bool "for" (Set (Var "x")) "," (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k")))) "iff" (Bool "(" (Bool (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool "(" (Bool (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "or" (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) ")" ) ")" ) ")" )))) ; theorem :: FLANG_3:47 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k"))))) "holds" (Bool (Set (Set (Var "B")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "B")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A")) ")" ) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k"))))))) ; begin definitionlet "E" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ); func "A" :::"+"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "E" ($#k8_afinsq_1 :::"^omega"::: ) ")" ) equals :: FLANG_3:def 2 (Set ($#k3_tarski :::"union"::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "E" ($#k8_afinsq_1 :::"^omega"::: ) ")" ) : (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set "A" ($#k7_flang_1 :::"|^"::: ) (Set (Var "n")))) ")" )) "}" ); end; :: deftheorem defines :::"+"::: FLANG_3:def 2 : (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set (Var "B")) where B "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) : (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n")))) ")" )) "}" )))); theorem :: FLANG_3:48 (Bool "for" (Set (Var "E")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) )) "iff" (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n")))) ")" )) ")" ))) ; theorem :: FLANG_3:49 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ))))) ; theorem :: FLANG_3:50 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Num 1))))) ; theorem :: FLANG_3:51 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "iff" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ; theorem :: FLANG_3:52 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A")))))) ; theorem :: FLANG_3:53 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ")" ))))) ; theorem :: FLANG_3:54 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k1_flang_2 :::"|^"::: ) "(" (Num 1) "," (Set (Var "n")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ")" )))))) ; theorem :: FLANG_3:55 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) )))) ; theorem :: FLANG_3:56 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "holds" (Bool "(" (Bool (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) )) "iff" (Bool (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ))) ; theorem :: FLANG_3:57 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) )) "iff" (Bool (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ))) ; theorem :: FLANG_3:58 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k2_flang_3 :::"+"::: ) )))) ; theorem :: FLANG_3:59 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) )))) ; theorem :: FLANG_3:60 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" ) ($#k2_flang_3 :::"+"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) )) & (Bool (Set (Set "(" (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ")" ) ($#k8_flang_1 :::"*"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) )) ")" ))) ; theorem :: FLANG_3:61 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k8_flang_1 :::"*"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k8_flang_1 :::"*"::: ) )))) ; theorem :: FLANG_3:62 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ")" ) ($#k2_flang_3 :::"+"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) )))) ; theorem :: FLANG_3:63 (Bool "for" (Set (Var "x")) "," (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))))) "holds" (Bool (Set (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )))) ; theorem :: FLANG_3:64 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) "iff" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k4_flang_1 :::"{"::: ) (Set "(" ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) ")" ))) ; theorem :: FLANG_3:65 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ")" ) ($#k2_flang_2 :::"?"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) )) & (Bool (Set (Set "(" (Set (Var "A")) ($#k2_flang_2 :::"?"::: ) ")" ) ($#k2_flang_3 :::"+"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) )) ")" ))) ; theorem :: FLANG_3:66 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "C")) ($#k2_flang_3 :::"+"::: ) )) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "C")) ($#k2_flang_3 :::"+"::: ) ))) "holds" (Bool (Set (Set (Var "a")) ($#k1_flang_1 :::"^"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "C")) ($#k2_flang_3 :::"+"::: ) ))))) ; theorem :: FLANG_3:67 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "C")) ($#k2_flang_3 :::"+"::: ) )) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "C")) ($#k2_flang_3 :::"+"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "C")) ($#k2_flang_3 :::"+"::: ) )))) ; theorem :: FLANG_3:68 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) )))) ; theorem :: FLANG_3:69 (Bool "for" (Set (Var "x")) "," (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "st" (Bool (Bool (Set (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E")))))) ; theorem :: FLANG_3:70 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A")))))) ; theorem :: FLANG_3:71 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "k")) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "k")) ")" )))))) ; theorem :: FLANG_3:72 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k1_flang_2 :::"|^"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k1_flang_2 :::"|^"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" )))))) ; theorem :: FLANG_3:73 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "st" (Bool (Bool (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "B")) ($#k2_flang_3 :::"+"::: ) ")" ))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "B")) ($#k2_flang_3 :::"+"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A")))) ")" ))) ; theorem :: FLANG_3:74 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Num 2))))) ; theorem :: FLANG_3:75 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set "(" (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )))))) ; theorem :: FLANG_3:76 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Num 2))))) ; theorem :: FLANG_3:77 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "k")) "," (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "l")))) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k1_flang_2 :::"|^"::: ) "(" (Set (Var "k")) "," (Set (Var "l")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set "(" (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )))))) ; theorem :: FLANG_3:78 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k2_flang_3 :::"+"::: ) )) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k7_flang_1 :::"|^"::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k2_flang_3 :::"+"::: ) ))))) ; theorem :: FLANG_3:79 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k2_flang_2 :::"?"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k2_flang_2 :::"?"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ")" ))))) ; theorem :: FLANG_3:80 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k2_flang_2 :::"?"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) )))) ; theorem :: FLANG_3:81 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k2_flang_2 :::"?"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) )) "iff" (Bool (Set ($#k2_flang_1 :::"<%>"::: ) (Set (Var "E"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ))) ; theorem :: FLANG_3:82 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k2_flang_3 :::"+"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k2_flang_3 :::"+"::: ) )))) ; theorem :: FLANG_3:83 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k2_flang_3 :::"+"::: ) ))) "holds" (Bool (Set (Set (Var "B")) ($#k2_flang_3 :::"+"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "B")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "A")) ")" ) ($#k2_flang_3 :::"+"::: ) )))) ; theorem :: FLANG_3:84 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ))))) ; theorem :: FLANG_3:85 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k1_flang_2 :::"|^"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ))))) ; theorem :: FLANG_3:86 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" ))))) ; theorem :: FLANG_3:87 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ")" ) ($#k7_flang_1 :::"|^"::: ) (Set (Var "k"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k"))))))) ; theorem :: FLANG_3:88 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ")" ) ($#k1_flang_2 :::"|^"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "m"))))))) ; theorem :: FLANG_3:89 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k2_flang_3 :::"+"::: ) )) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "n"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "B")) ($#k2_flang_3 :::"+"::: ) ))))) ; theorem :: FLANG_3:90 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set "(" (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )))))) ; theorem :: FLANG_3:91 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k1_flang_3 :::"|^.."::: ) (Set (Var "k")) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ")" )))))) ; theorem :: FLANG_3:92 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) )))) ; theorem :: FLANG_3:93 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "st" (Bool (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k8_flang_1 :::"*"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ")" ) ($#k6_flang_1 :::"^^"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) )) & (Bool (Set (Set (Var "B")) ($#k6_flang_1 :::"^^"::: ) (Set "(" (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) )) ")" ))) ; theorem :: FLANG_3:94 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" ) ($#k2_flang_3 :::"+"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "B")) ($#k2_flang_3 :::"+"::: ) ")" ))))) ; theorem :: FLANG_3:95 (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "B")) ($#k2_flang_3 :::"+"::: ) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" ) ($#k2_flang_3 :::"+"::: ) )))) ; theorem :: FLANG_3:96 (Bool "for" (Set (Var "E")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "E")) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "holds" (Bool "(" (Bool (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "A")) ($#k2_flang_3 :::"+"::: ) )) "iff" (Bool (Set ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ))) ;