:: FLANG_2  semantic presentation begin  
























theorem :: FLANG_2:1 (Bool  "for" (Set (Var "m")) "," (Set (Var "k")) "," (Set (Var "i")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k"))))) "holds"  (Bool  "ex" (Set (Var "mn")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "("  (Bool (Set (Set (Var "mn"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Var "i"))) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "mn"))) & (Bool (Set (Var "mn"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))  ")" ))) ; 
 
theorem :: FLANG_2:2 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "l")) "," (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "l"))) & (Bool (Set (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "l"))))) "holds"  (Bool  "ex" (Set (Var "mn")) "," (Set (Var "kl")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "("  (Bool (Set (Set (Var "mn"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "kl")))  ($#r1_hidden :::"="::: )  (Set (Var "i"))) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "mn"))) & (Bool (Set (Var "mn"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "kl"))) & (Bool (Set (Var "kl"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "l")))  ")" ))) ; 
 
theorem :: FLANG_2:3 (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  "ex" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "("  (Bool (Set (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ))) ; 
 
theorem :: FLANG_2:4 (Bool  "for" (Set (Var "E")) "being"    ($#m1_hidden :::"set"::: )    (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  "("  (Bool (Set (Set (Var "a"))  ($#k1_flang_1 :::"^"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) "or" (Bool (Set (Set (Var "b"))  ($#k1_flang_1 :::"^"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" )) "holds"  (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))) ; 
 begin  
theorem :: FLANG_2:5 (Bool  "for" (Set (Var "x")) "," (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  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) "or" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))  ")" ) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E"))))) "holds"  (Bool (Set (Set (Var "A"))  ($#k6_flang_1 :::"^^"::: )  (Set (Var "B")))  ($#r1_hidden :::"<>"::: )  (Set  ($#k4_flang_1 :::"{"::: ) (Set  "("  ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )))) ; 
 
theorem :: FLANG_2:6 (Bool  "for" (Set (Var "x")) "," (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  "("  (Bool (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k6_flang_1 :::"^^"::: )  (Set (Var "B")))) "iff" (Bool  "("  (Bool  "("  (Bool (Set   ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E")))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "B")))  ")" ) "or" (Bool  "("  (Bool (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set   ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E")))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))  ")" )  ")" )  ")" ))) ; 
 
theorem :: FLANG_2:7 (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")))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "n")))  ($#r1_hidden :::"<>"::: )  (Set  ($#k4_flang_1 :::"{"::: ) (Set  "("  ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) ))))) ; 
 
theorem :: FLANG_2: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  "("  (Bool (Set   ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E")))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (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_2:9 (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":::) "holds"   (Bool  "("  (Bool (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "n")))) "iff" (Bool  "("  (Bool (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool  "("  (Bool  "("  (Bool (Set   ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E")))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Num 1))  ")" ) "or" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )  ")" )  ")" )))) ; 
 
theorem :: FLANG_2:10 (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 "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_hidden :::"<>"::: )  (Set (Var "n"))) & (Bool (Set (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "n")))  ($#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_2: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 "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "m")) ")" )  ($#k7_flang_1 :::"|^"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "n")) ")" )  ($#k7_flang_1 :::"|^"::: )  (Set (Var "m"))))))) ; 
 
theorem :: FLANG_2: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 "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "m")) ")" )  ($#k6_flang_1 :::"^^"::: )  (Set  "(" (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "n")) ")" )  ($#k6_flang_1 :::"^^"::: )  (Set  "(" (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "m")) ")" )))))) ; 
 
theorem :: FLANG_2:13 (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 "l")) "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"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "l")) ")" ))) & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Set  "(" (Set (Var "B"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "l")) ")" )  ($#k6_flang_1 :::"^^"::: )  (Set (Var "A"))))  ")" )))) ; 
 
theorem :: FLANG_2:14 (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 "k")) "," (Set (Var "l")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "C"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "k")))) & (Bool (Set (Var "B"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "C"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "l"))))) "holds"  (Bool (Set (Set (Var "A"))  ($#k6_flang_1 :::"^^"::: )  (Set (Var "B")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "C"))  ($#k7_flang_1 :::"|^"::: )  (Set  "(" (Set (Var "k"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "l")) ")" )))))) ; 
 
theorem :: FLANG_2:15 (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"))  ($#k8_flang_1 :::"*"::: )  )  ($#r1_hidden :::"<>"::: )  (Set  ($#k4_flang_1 :::"{"::: ) (Set  "("  ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )))) ; 
 
theorem :: FLANG_2: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":::)  "st" (Bool (Bool (Set   ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E")))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "n")) ")" )  ($#k8_flang_1 :::"*"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k8_flang_1 :::"*"::: )  ))))) ; 
 
theorem :: FLANG_2: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 "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set   ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E")))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "n")) ")" )  ($#k8_flang_1 :::"*"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k8_flang_1 :::"*"::: )  ")" )  ($#k7_flang_1 :::"|^"::: )  (Set (Var "n"))))))) ; 
 
theorem :: FLANG_2:18 (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  "("  (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "A"))  ($#k6_flang_1 :::"^^"::: )  (Set  "(" (Set (Var "B"))  ($#k8_flang_1 :::"*"::: )  ")" ))) & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Set  "(" (Set (Var "B"))  ($#k8_flang_1 :::"*"::: )  ")" )  ($#k6_flang_1 :::"^^"::: )  (Set (Var "A"))))  ")" ))) ; 
 begin  definitionlet "E" be    ($#m1_hidden :::"set"::: )  ; let "A" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Const "E"))  ($#k8_afinsq_1 :::"^omega"::: )  ")" ); let "m", "n" be   ($#m1_hidden :::"Nat":::); func "A" :::"|^":::  "(" "m" "," "n" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" "E"  ($#k8_afinsq_1 :::"^omega"::: )  ")" ) equals :: FLANG_2: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 "k")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "("  (Bool "m"  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  "n") & (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set "A"  ($#k7_flang_1 :::"|^"::: )  (Set (Var "k"))))  ")" ))  "}"  ); end; 








:: deftheorem    defines :::"|^"::: FLANG_2: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 "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (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 "k")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "("  (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "k"))))  ")" ))  "}"  ))))); 
 
theorem :: FLANG_2:19 (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 "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )) "iff" (Bool  "ex" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "("  (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "k"))))  ")" ))  ")" )))) ; 
 
theorem :: FLANG_2: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 "m")) "," (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "k")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" ))))) ; 
 
theorem :: FLANG_2:21 (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  "("  (Bool (Set (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "iff" (Bool  "("  (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "n"))) "or" (Bool  "("  (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )  ")" )  ")" )))) ; 
 
theorem :: FLANG_2: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 "m")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "m")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "m"))))))) ; 
 
theorem :: FLANG_2: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 "m")) "," (Set (Var "k")) "," (Set (Var "l")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "l"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "k")) "," (Set (Var "l")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" ))))) ; 
 
theorem :: FLANG_2: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 "m")) "," (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "k")) ")"  ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "k")) "," (Set (Var "n")) ")"  ")" )))))) ; 
 
theorem :: FLANG_2: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 "m")) "," (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "k")) ")"  ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set  "(" (Set (Var "k"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "n")) ")"  ")" )))))) ; 
 
theorem :: FLANG_2:26 (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 (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) ")" )))))) ; 
 
theorem :: FLANG_2: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":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "m")) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) "," (Set (Var "n")) ")"  ")" )))))) ; 
 
theorem :: FLANG_2:28 (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_2 :::"|^"::: )   "(" (Set (Var "n")) "," (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "n")) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) ")" )))))) ; 
 
theorem :: FLANG_2: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 "m")) "," (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_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Set (Var "B"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" ))))) ; 
 
theorem :: FLANG_2:30 (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 "m")) "," (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")))) & (Bool  "("  (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool (Set (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )  ($#r1_hidden :::"<>"::: )  (Set  ($#k4_flang_1 :::"{"::: ) (Set  "("  ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) ))))) ; 
 
theorem :: FLANG_2: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 "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k4_flang_1 :::"{"::: ) (Set  "("  ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )) "iff" (Bool  "("  (Bool  "("  (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (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 "m"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )  ")" )  ")" )))) ; 
 
theorem :: FLANG_2: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")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Set (Var "A"))  ($#k8_flang_1 :::"*"::: )  ))))) ; 
 
theorem :: FLANG_2: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 "m")) "," (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_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool  "("  (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set   ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E")))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))  ")" )  ")" )  ")" )))) ; 
 
theorem :: FLANG_2: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 "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set   ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E")))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "n"))))))) ; 
 
theorem :: FLANG_2: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")) "," (Set (Var "k")) "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"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "k")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "k")) ")" )  ($#k6_flang_1 :::"^^"::: )  (Set  "(" (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )))))) ; 
 
theorem :: FLANG_2: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"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k6_flang_1 :::"^^"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k6_flang_1 :::"^^"::: )  (Set  "(" (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )))))) ; 
 
theorem :: FLANG_2:37 (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")) "," (Set (Var "k")) "," (Set (Var "l")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "l")))) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (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_2 :::"|^"::: )   "(" (Set  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k")) ")" ) "," (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "l")) ")" ) ")" ))))) ; 
 
theorem :: FLANG_2:38 (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 (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) "," (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k6_flang_1 :::"^^"::: )  (Set (Var "A"))))))) ; 
 
theorem :: FLANG_2:39 (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")) "," (Set (Var "k")) "," (Set (Var "l")) "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"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "k")) "," (Set (Var "l")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "k")) "," (Set (Var "l")) ")"  ")" )  ($#k6_flang_1 :::"^^"::: )  (Set  "(" (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )))))) ; 
 
theorem :: FLANG_2: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 "m")) "," (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k7_flang_1 :::"|^"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set  "(" (Set (Var "m"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "k")) ")" ) "," (Set  "(" (Set (Var "n"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "k")) ")" ) ")" ))))) ; 
 
theorem :: FLANG_2: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")) "," (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set  "(" (Set (Var "k"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Set  "(" (Set  "(" (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "k")) ")" )  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k6_flang_1 :::"^^"::: )  (Set  "(" (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )))))) ; 
 
theorem :: FLANG_2: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")) "," (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "k")) ")" )  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set  "(" (Set (Var "k"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "m")) ")" ) "," (Set  "(" (Set (Var "k"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "n")) ")" ) ")" ))))) ; 
 
theorem :: FLANG_2:43 (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":::) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "k")) ")" )  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k7_flang_1 :::"|^"::: )  (Set (Var "k"))))))) ; 
 
theorem :: FLANG_2:44 (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 "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set  "(" (Set (Var "k"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "l")) ")" ) ")" )  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Set  "(" (Set  "(" (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "k")) ")" )  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k6_flang_1 :::"^^"::: )  (Set  "(" (Set  "(" (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "l")) ")" )  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )))))) ; 
 
theorem :: FLANG_2:45 (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"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k4_flang_1 :::"{"::: ) (Set  "("  ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )))) ; 
 
theorem :: FLANG_2:46 (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"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k4_flang_1 :::"{"::: ) (Set  "("  ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set (Var "A")))))) ; 
 
theorem :: FLANG_2:47 (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"))  ($#k1_flang_2 :::"|^"::: )   "(" (Num 1) "," (Num 1) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "A"))))) ; 
 
theorem :: FLANG_2:48 (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"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 2) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  ($#k4_flang_1 :::"{"::: ) (Set  "("  ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set (Var "A")) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set (Var "A"))  ($#k6_flang_1 :::"^^"::: )  (Set (Var "A")) ")" ))))) ; 
 
theorem :: FLANG_2: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"::: )  ")" ) "holds"  (Bool (Set (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Num 1) "," (Num 2) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set (Var "A"))  ($#k6_flang_1 :::"^^"::: )  (Set (Var "A")) ")" ))))) ; 
 
theorem :: FLANG_2: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"))  ($#k1_flang_2 :::"|^"::: )   "(" (Num 2) "," (Num 2) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k6_flang_1 :::"^^"::: )  (Set (Var "A")))))) ; 
 
theorem :: FLANG_2:51 (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 "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) "holds"  (Bool  "for" (Set (Var "mn")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "mn"))) & (Bool (Set (Var "mn"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "mn")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )))))) ; 
 
theorem :: FLANG_2:52 (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 "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_hidden :::"<>"::: )  (Set (Var "n"))) & (Bool (Set (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )  ($#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_2:53 (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 "m")) "," (Set (Var "n")) "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_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )) "iff" (Bool  "("  (Bool (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool  "("  (Bool  "("  (Bool (Set   ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E")))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1)) & (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))  ")" )  ")" )  ")" )  ")" )))) ; 
 
theorem :: FLANG_2:54 (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 "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B")) ")" )  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "(" (Set (Var "B"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )))))) ; 
 
theorem :: FLANG_2:55 (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 "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set (Var "B"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" ))  ($#r1_tarski :::"c="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" )  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" ))))) ; 
 
theorem :: FLANG_2: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"::: )  ")" )  (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "l")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "k")) "," (Set (Var "l")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set  "(" (Set (Var "m"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "k")) ")" ) "," (Set  "(" (Set (Var "n"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "l")) ")" ) ")" ))))) ; 
 
theorem :: FLANG_2:57 (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 "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (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_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" ))) & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Set  "(" (Set (Var "B"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k6_flang_1 :::"^^"::: )  (Set (Var "A"))))  ")" )))) ; 
 
theorem :: FLANG_2:58 (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")) "," (Set (Var "k")) "," (Set (Var "l")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "l"))) & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "C"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )) & (Bool (Set (Var "B"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "C"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "k")) "," (Set (Var "l")) ")" ))) "holds"  (Bool (Set (Set (Var "A"))  ($#k6_flang_1 :::"^^"::: )  (Set (Var "B")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "C"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "k")) ")" ) "," (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "l")) ")" ) ")" ))))) ; 
 
theorem :: FLANG_2: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"::: )  ")" )  (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")) ")"  ")" )  ($#k8_flang_1 :::"*"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Set (Var "A"))  ($#k8_flang_1 :::"*"::: )  ))))) ; 
 
theorem :: FLANG_2: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"::: )  ")" )  (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k8_flang_1 :::"*"::: )  ")" )  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Set (Var "A"))  ($#k8_flang_1 :::"*"::: )  ))))) ; 
 
theorem :: FLANG_2:61 (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"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k8_flang_1 :::"*"::: )  ")" )  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k8_flang_1 :::"*"::: )  ))))) ; 
 
theorem :: FLANG_2: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"::: )  ")" )  (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E")))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k8_flang_1 :::"*"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k8_flang_1 :::"*"::: )  ))))) ; 
 
theorem :: FLANG_2:63 (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"))) & (Bool (Set   ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E")))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k8_flang_1 :::"*"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k8_flang_1 :::"*"::: )  ")" )  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" ))))) ; 
 
theorem :: FLANG_2:64 (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 "m")) "," (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_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Set (Var "B"))  ($#k8_flang_1 :::"*"::: )  ))))) ; 
 
theorem :: FLANG_2:65 (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 "m")) "," (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 "B"))  ($#k8_flang_1 :::"*"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "B"))  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" ) ")" )  ($#k8_flang_1 :::"*"::: )  ))))) ; 
 
theorem :: FLANG_2:66 (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"))  ($#k8_flang_1 :::"*"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k8_flang_1 :::"*"::: )  ")" )  ($#k6_flang_1 :::"^^"::: )  (Set  "(" (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )))))) ; 
 
theorem :: FLANG_2:67 (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   ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E")))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (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_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )))))) ; 
 
theorem :: FLANG_2: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"::: )  ")" )  (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k7_flang_1 :::"|^"::: )  (Set (Var "k")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "A"))  ($#k8_flang_1 :::"*"::: )  ))))) ; 
 
theorem :: FLANG_2:69 (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":::) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "k")) ")" )  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Set (Var "A"))  ($#k8_flang_1 :::"*"::: )  ))))) ; 
 
theorem :: FLANG_2: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"::: )  ")" )  (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  "(" (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "m")) ")" )  ($#k8_flang_1 :::"*"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k8_flang_1 :::"*"::: )  ))))) ; 
 
theorem :: FLANG_2: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 "m")) "," (Set (Var "n")) "," (Set (Var "k")) "," (Set (Var "l")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "k")) "," (Set (Var "l")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Set (Var "A"))  ($#k8_flang_1 :::"*"::: )  ))))) ; 
 
theorem :: FLANG_2: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 "k")) "," (Set (Var "n")) "," (Set (Var "l")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set   ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E")))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "l"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "k")) "," (Set (Var "n")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "l")) "," (Set (Var "n")) ")" ))))) ; 
 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_2: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 "k")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "("  (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1)) & (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set "A"  ($#k7_flang_1 :::"|^"::: )  (Set (Var "k"))))  ")" ))  "}"  ); end; 






:: deftheorem    defines :::"?"::: FLANG_2: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_2 :::"?"::: )  )  ($#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 "k")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "("  (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1)) & (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "k"))))  ")" ))  "}"  )))); 
 
theorem :: FLANG_2:73 (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_2 :::"?"::: )  )) "iff" (Bool  "ex" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "("  (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1)) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "k"))))  ")" ))  ")" ))) ; 
 
theorem :: FLANG_2: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"::: )  ")" )  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "n")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "A"))  ($#k2_flang_2 :::"?"::: )  ))))) ; 
 
theorem :: FLANG_2: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"::: )  ")" ) "holds"  (Bool (Set (Set (Var "A"))  ($#k2_flang_2 :::"?"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Num 1) ")" ))))) ; 
 
theorem :: FLANG_2: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 (Var "A"))  ($#k2_flang_2 :::"?"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k4_flang_1 :::"{"::: ) (Set  "("  ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set (Var "A")))))) ; 
 
theorem :: FLANG_2: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"::: )  ")" ) "holds"  (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "A"))  ($#k2_flang_2 :::"?"::: )  )))) ; 
 
theorem :: FLANG_2:78 (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"::: )  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k2_flang_2 :::"?"::: )  )) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E")))) "or" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))  ")" )  ")" ))) ; 
 
theorem :: FLANG_2: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 (Var "A"))  ($#k2_flang_2 :::"?"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" )))) ; 
 
theorem :: FLANG_2: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  "("  (Bool (Set (Set (Var "A"))  ($#k2_flang_2 :::"?"::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "A"))) "iff" (Bool (Set   ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E")))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))  ")" ))) ; 
 registrationlet "E" be    ($#m1_hidden :::"set"::: )  ; let "A" be   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Const "E"))  ($#k8_afinsq_1 :::"^omega"::: )  ")" ); 
cluster (Set "A"  ($#k2_flang_2 :::"?"::: )  ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: FLANG_2: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 (Set (Set  "(" (Set (Var "A"))  ($#k2_flang_2 :::"?"::: )  ")" )  ($#k2_flang_2 :::"?"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k2_flang_2 :::"?"::: )  )))) ; 
 
theorem :: FLANG_2: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 (Var "B")))) "holds"  (Bool (Set (Set (Var "A"))  ($#k2_flang_2 :::"?"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Set (Var "B"))  ($#k2_flang_2 :::"?"::: )  )))) ; 
 
theorem :: FLANG_2:83 (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_2 :::"?"::: )  )  ($#r1_hidden :::"<>"::: )  (Set  ($#k4_flang_1 :::"{"::: ) (Set  "("  ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) )))) ; 
 
theorem :: FLANG_2: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"::: )  ")" ) "holds"   (Bool  "("  (Bool (Set (Set (Var "A"))  ($#k2_flang_2 :::"?"::: )  )  ($#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   ($#k1_xboole_0 :::"{}"::: )  )) "or" (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_flang_1 :::"{"::: ) (Set  "("  ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) ))  ")" )  ")" ))) ; 
 
theorem :: FLANG_2: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"::: )  ")" ) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k8_flang_1 :::"*"::: )  ")" )  ($#k2_flang_2 :::"?"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k8_flang_1 :::"*"::: )  )) & (Bool (Set (Set  "(" (Set (Var "A"))  ($#k2_flang_2 :::"?"::: )  ")" )  ($#k8_flang_1 :::"*"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k8_flang_1 :::"*"::: )  ))  ")" ))) ; 
 
theorem :: FLANG_2: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 (Var "A"))  ($#k2_flang_2 :::"?"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Set (Var "A"))  ($#k8_flang_1 :::"*"::: )  )))) ; 
 
theorem :: FLANG_2:87 (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_2 :::"?"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k2_flang_2 :::"?"::: )  ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "(" (Set (Var "B"))  ($#k2_flang_2 :::"?"::: )  ")" ))))) ; 
 
theorem :: FLANG_2:88 (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_2 :::"?"::: )  ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set (Var "B"))  ($#k2_flang_2 :::"?"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" )  ($#k2_flang_2 :::"?"::: )  )))) ; 
 
theorem :: FLANG_2:89 (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_2 :::"?"::: )  )  ($#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_2:90 (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_2 :::"?"::: )  )) "iff" (Bool (Set  ($#k5_afinsq_1 :::"<%"::: ) (Set (Var "x")) ($#k5_afinsq_1 :::"%>"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "A")))  ")" ))) ; 
 
theorem :: FLANG_2: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"::: )  ")" ) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k2_flang_2 :::"?"::: )  ")" )  ($#k6_flang_1 :::"^^"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k6_flang_1 :::"^^"::: )  (Set  "(" (Set (Var "A"))  ($#k2_flang_2 :::"?"::: )  ")" ))))) ; 
 
theorem :: FLANG_2: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_2 :::"?"::: )  ")" )  ($#k6_flang_1 :::"^^"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Num 1) "," (Num 2) ")" )))) ; 
 
theorem :: FLANG_2:93 (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_2 :::"?"::: )  ")" )  ($#k6_flang_1 :::"^^"::: )  (Set  "(" (Set (Var "A"))  ($#k2_flang_2 :::"?"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 2) ")" )))) ; 
 
theorem :: FLANG_2:94 (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_2 :::"?"::: )  ")" )  ($#k7_flang_1 :::"|^"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k2_flang_2 :::"?"::: )  ")" )  ($#k1_flang_2 :::"|^"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "k")) ")" ))))) ; 
 
theorem :: FLANG_2:95 (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_2 :::"?"::: )  ")" )  ($#k7_flang_1 :::"|^"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "k")) ")" ))))) ; 
 
theorem :: FLANG_2:96 (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  "(" (Set (Var "A"))  ($#k2_flang_2 :::"?"::: )  ")" )  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k2_flang_2 :::"?"::: )  ")" )  ($#k1_flang_2 :::"|^"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n")) ")" ))))) ; 
 
theorem :: FLANG_2:97 (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"))  ($#k2_flang_2 :::"?"::: )  ")" )  ($#k1_flang_2 :::"|^"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n")) ")" ))))) ; 
 
theorem :: FLANG_2:98 (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  "(" (Set (Var "A"))  ($#k2_flang_2 :::"?"::: )  ")" )  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n")) ")" ))))) ; 
 
theorem :: FLANG_2:99 (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_2 :::"|^"::: )   "(" (Num 1) "," (Set (Var "n")) ")"  ")" )  ($#k2_flang_2 :::"?"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "n")) ")" ))))) ; 
 
theorem :: FLANG_2:100 (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   ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E")))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set   ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E")))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "A"))  ($#k2_flang_2 :::"?"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Set (Var "A"))  ($#k6_flang_1 :::"^^"::: )  (Set (Var "B")))) & (Bool (Set (Set (Var "A"))  ($#k2_flang_2 :::"?"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Set (Var "B"))  ($#k6_flang_1 :::"^^"::: )  (Set (Var "A"))))  ")" ))) ; 
 
theorem :: FLANG_2:101 (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  "("  (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "A"))  ($#k6_flang_1 :::"^^"::: )  (Set  "(" (Set (Var "B"))  ($#k2_flang_2 :::"?"::: )  ")" ))) & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Set  "(" (Set (Var "B"))  ($#k2_flang_2 :::"?"::: )  ")" )  ($#k6_flang_1 :::"^^"::: )  (Set (Var "A"))))  ")" ))) ; 
 
theorem :: FLANG_2:102 (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_2 :::"?"::: )  )) & (Bool (Set (Var "B"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "C"))  ($#k2_flang_2 :::"?"::: )  ))) "holds"  (Bool (Set (Set (Var "A"))  ($#k6_flang_1 :::"^^"::: )  (Set (Var "B")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "C"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 2) ")" )))) ; 
 
theorem :: FLANG_2:103 (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   ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E")))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "A"))  ($#k2_flang_2 :::"?"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "n"))))))) ; 
 
theorem :: FLANG_2:104 (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_2 :::"?"::: )  ")" )  ($#k6_flang_1 :::"^^"::: )  (Set  "(" (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "k")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "k")) ")" )  ($#k6_flang_1 :::"^^"::: )  (Set  "(" (Set (Var "A"))  ($#k2_flang_2 :::"?"::: )  ")" )))))) ; 
 
theorem :: FLANG_2:105 (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_2 :::"?"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Set (Var "B"))  ($#k8_flang_1 :::"*"::: )  )))) ; 
 
theorem :: FLANG_2:106 (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 "B"))  ($#k8_flang_1 :::"*"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "B"))  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set (Var "A"))  ($#k2_flang_2 :::"?"::: )  ")" ) ")" )  ($#k8_flang_1 :::"*"::: )  )))) ; 
 
theorem :: FLANG_2:107 (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_2 :::"?"::: )  ")" )  ($#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"))  ($#k2_flang_2 :::"?"::: )  ")" ))))) ; 
 
theorem :: FLANG_2:108 (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_2 :::"?"::: )  ")" )  ($#k6_flang_1 :::"^^"::: )  (Set  "(" (Set (Var "A"))  ($#k8_flang_1 :::"*"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k8_flang_1 :::"*"::: )  )))) ; 
 
theorem :: FLANG_2:109 (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_2 :::"?"::: )  ")" )  ($#k7_flang_1 :::"|^"::: )  (Set (Var "k")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "A"))  ($#k8_flang_1 :::"*"::: )  ))))) ; 
 
theorem :: FLANG_2:110 (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")) ")" )  ($#k2_flang_2 :::"?"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Set (Var "A"))  ($#k8_flang_1 :::"*"::: )  ))))) ; 
 
theorem :: FLANG_2:111 (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_2 :::"?"::: )  ")" )  ($#k6_flang_1 :::"^^"::: )  (Set  "(" (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")"  ")" )  ($#k6_flang_1 :::"^^"::: )  (Set  "(" (Set (Var "A"))  ($#k2_flang_2 :::"?"::: )  ")" )))))) ; 
 
theorem :: FLANG_2:112 (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_2 :::"?"::: )  ")" )  ($#k6_flang_1 :::"^^"::: )  (Set  "(" (Set (Var "A"))  ($#k7_flang_1 :::"|^"::: )  (Set (Var "k")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "k")) "," (Set  "(" (Set (Var "k"))  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" ) ")" ))))) ; 
 
theorem :: FLANG_2:113 (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_2 :::"?"::: )  ")" )  ($#k1_flang_2 :::"|^"::: )   "(" (Set (Var "m")) "," (Set (Var "n")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Set (Var "A"))  ($#k8_flang_1 :::"*"::: )  ))))) ; 
 
theorem :: FLANG_2:114 (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")) ")"  ")" )  ($#k2_flang_2 :::"?"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Set (Var "A"))  ($#k8_flang_1 :::"*"::: )  ))))) ; 
 
theorem :: FLANG_2:115 (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_2 :::"?"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k7_subset_1 :::"\"::: )  (Set  ($#k4_flang_1 :::"{"::: ) (Set  "("  ($#k2_flang_1 :::"<%>"::: )  (Set (Var "E")) ")" ) ($#k4_flang_1 :::"}"::: ) ) ")" )  ($#k2_flang_2 :::"?"::: )  )))) ; 
 
theorem :: FLANG_2:116 (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_2 :::"?"::: )  ))) "holds"  (Bool (Set (Set (Var "A"))  ($#k2_flang_2 :::"?"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Set (Var "B"))  ($#k2_flang_2 :::"?"::: )  )))) ; 
 
theorem :: FLANG_2:117 (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_2 :::"?"::: )  ))) "holds"  (Bool (Set (Set (Var "B"))  ($#k2_flang_2 :::"?"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "B"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "A")) ")" )  ($#k2_flang_2 :::"?"::: )  )))) ;