:: ZFMODEL2 semantic presentation begin theorem :: ZFMODEL2:1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool (Set ($#k2_zf_model :::"Free"::: ) (Set "(" (Set (Var "H")) ($#k6_zf_lang1 :::"/"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k2_zf_model :::"Free"::: ) (Set (Var "H")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: ZFMODEL2:2 (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k4_zf_lang1 :::"variables_in"::: ) (Set (Var "H")))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H"))))) "implies" (Bool (Set ($#k2_zf_model :::"Free"::: ) (Set "(" (Set (Var "H")) ($#k6_zf_lang1 :::"/"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_zf_model :::"Free"::: ) (Set (Var "H")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H")))))) "implies" (Bool (Set ($#k2_zf_model :::"Free"::: ) (Set "(" (Set (Var "H")) ($#k6_zf_lang1 :::"/"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H")))) ")" ")" ))) ; registrationlet "H" be ($#m2_finseq_1 :::"ZF-formula":::); cluster (Set ($#k3_zf_lang1 :::"variables_in"::: ) "H") -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: ZFMODEL2:3 (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "holds" (Bool "(" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k2_zf_lang :::"x."::: ) (Set (Var "j"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_zf_lang1 :::"variables_in"::: ) (Set (Var "H"))))) "holds" (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))))) & (Bool "not" (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_zf_lang1 :::"variables_in"::: ) (Set (Var "H")))))) ")" )) ; theorem :: ZFMODEL2:4 (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_zf_lang1 :::"variables_in"::: ) (Set (Var "H")))))) "holds" (Bool "(" (Bool (Set (Var "M")) "," (Set (Var "v")) ($#r1_zf_model :::"|="::: ) (Set (Var "H"))) "iff" (Bool (Set (Var "M")) "," (Set (Var "v")) ($#r1_zf_model :::"|="::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set (Var "x")) "," (Set (Var "H")) ")" )) ")" ))))) ; theorem :: ZFMODEL2:5 (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "M")) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_zf_lang1 :::"variables_in"::: ) (Set (Var "H")))))) "holds" (Bool "(" (Bool (Set (Var "M")) "," (Set (Var "v")) ($#r1_zf_model :::"|="::: ) (Set (Var "H"))) "iff" (Bool (Set (Var "M")) "," (Set (Set (Var "v")) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x")) "," (Set (Var "m")) ")" ) ($#r1_zf_model :::"|="::: ) (Set (Var "H"))) ")" )))))) ; theorem :: ZFMODEL2:6 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "," (Set (Var "m3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "M")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set (Var "z"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x")))) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set (Var "v")) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x")) "," (Set (Var "m1")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "y")) "," (Set (Var "m2")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "z")) "," (Set (Var "m3")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "v")) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "z")) "," (Set (Var "m3")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "y")) "," (Set (Var "m2")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x")) "," (Set (Var "m1")) ")" )) & (Bool (Set (Set "(" (Set "(" (Set (Var "v")) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x")) "," (Set (Var "m1")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "y")) "," (Set (Var "m2")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "z")) "," (Set (Var "m3")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "v")) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "y")) "," (Set (Var "m2")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "z")) "," (Set (Var "m3")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x")) "," (Set (Var "m1")) ")" )) ")" ))))) ; theorem :: ZFMODEL2:7 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "," (Set (Var "m3")) "," (Set (Var "m4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "M")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x3"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x4"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"<>"::: ) (Set (Var "x3"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"<>"::: ) (Set (Var "x4"))) & (Bool (Set (Var "x3")) ($#r1_hidden :::"<>"::: ) (Set (Var "x4")))) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "v")) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x1")) "," (Set (Var "m1")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x2")) "," (Set (Var "m2")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x3")) "," (Set (Var "m3")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x4")) "," (Set (Var "m4")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "v")) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x2")) "," (Set (Var "m2")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x3")) "," (Set (Var "m3")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x4")) "," (Set (Var "m4")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x1")) "," (Set (Var "m1")) ")" )) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "v")) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x1")) "," (Set (Var "m1")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x2")) "," (Set (Var "m2")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x3")) "," (Set (Var "m3")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x4")) "," (Set (Var "m4")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "v")) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x3")) "," (Set (Var "m3")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x4")) "," (Set (Var "m4")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x1")) "," (Set (Var "m1")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x2")) "," (Set (Var "m2")) ")" )) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "v")) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x1")) "," (Set (Var "m1")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x2")) "," (Set (Var "m2")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x3")) "," (Set (Var "m3")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x4")) "," (Set (Var "m4")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "v")) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x4")) "," (Set (Var "m4")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x2")) "," (Set (Var "m2")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x3")) "," (Set (Var "m3")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x1")) "," (Set (Var "m1")) ")" )) ")" ))))) ; theorem :: ZFMODEL2:8 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "," (Set (Var "m")) "," (Set (Var "m3")) "," (Set (Var "m4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "M")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set (Var "v")) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x1")) "," (Set (Var "m1")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x2")) "," (Set (Var "m2")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x1")) "," (Set (Var "m")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x2")) "," (Set (Var "m2")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x1")) "," (Set (Var "m")) ")" )) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "v")) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x1")) "," (Set (Var "m1")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x2")) "," (Set (Var "m2")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x3")) "," (Set (Var "m3")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x1")) "," (Set (Var "m")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "v")) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x2")) "," (Set (Var "m2")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x3")) "," (Set (Var "m3")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x1")) "," (Set (Var "m")) ")" )) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "v")) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x1")) "," (Set (Var "m1")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x2")) "," (Set (Var "m2")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x3")) "," (Set (Var "m3")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x4")) "," (Set (Var "m4")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x1")) "," (Set (Var "m")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "v")) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x2")) "," (Set (Var "m2")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x3")) "," (Set (Var "m3")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x4")) "," (Set (Var "m4")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x1")) "," (Set (Var "m")) ")" )) ")" ))))) ; theorem :: ZFMODEL2:9 (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "M")) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H")))))) "holds" (Bool "(" (Bool (Set (Var "M")) "," (Set (Var "v")) ($#r1_zf_model :::"|="::: ) (Set (Var "H"))) "iff" (Bool (Set (Var "M")) "," (Set (Set (Var "v")) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x")) "," (Set (Var "m")) ")" ) ($#r1_zf_model :::"|="::: ) (Set (Var "H"))) ")" )))))) ; theorem :: ZFMODEL2:10 (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "st" (Bool (Bool (Bool "not" (Set ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H"))))) & (Bool (Set (Var "M")) "," (Set (Var "v")) ($#r1_zf_model :::"|="::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set "(" ($#k13_zf_lang :::"Ex"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) "," (Set "(" (Set (Var "H")) ($#k12_zf_lang :::"<=>"::: ) (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) ($#k4_zf_lang :::"'='"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ) ")" ")" ) ")" ")" ) ")" ))) "holds" (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_zfmodel1 :::"def_func'"::: ) "(" (Set (Var "H")) "," (Set (Var "v")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "m1"))) ($#r1_hidden :::"="::: ) (Set (Var "m2"))) "iff" (Bool (Set (Var "M")) "," (Set (Set "(" (Set (Var "v")) ($#k2_zf_lang1 :::"/"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set (Var "m1")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) "," (Set (Var "m2")) ")" ) ($#r1_zf_model :::"|="::: ) (Set (Var "H"))) ")" ))))) ; theorem :: ZFMODEL2:11 (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "st" (Bool (Bool (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) ($#k2_tarski :::"}"::: ) )) & (Bool (Set (Var "M")) ($#r2_zf_model :::"|="::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set "(" ($#k13_zf_lang :::"Ex"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) "," (Set "(" (Set (Var "H")) ($#k12_zf_lang :::"<=>"::: ) (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) ($#k4_zf_lang :::"'='"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ) ")" ")" ) ")" ")" ) ")" ))) "holds" (Bool (Set ($#k1_zfmodel1 :::"def_func'"::: ) "(" (Set (Var "H")) "," (Set (Var "v")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k2_zfmodel1 :::"def_func"::: ) "(" (Set (Var "H")) "," (Set (Var "M")) ")" ))))) ; theorem :: ZFMODEL2:12 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_zf_lang1 :::"variables_in"::: ) (Set (Var "H")))))) "holds" (Bool "(" (Bool (Set (Var "M")) "," (Set (Var "v")) ($#r1_zf_model :::"|="::: ) (Set (Set (Var "H")) ($#k6_zf_lang1 :::"/"::: ) "(" (Set (Var "y")) "," (Set (Var "x")) ")" )) "iff" (Bool (Set (Var "M")) "," (Set (Set (Var "v")) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "y")) "," (Set "(" (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#r1_zf_model :::"|="::: ) (Set (Var "H"))) ")" ))))) ; theorem :: ZFMODEL2:13 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_zf_lang1 :::"variables_in"::: ) (Set (Var "H"))))) & (Bool (Set (Var "M")) "," (Set (Var "v")) ($#r1_zf_model :::"|="::: ) (Set (Var "H")))) "holds" (Bool (Set (Var "M")) "," (Set (Set (Var "v")) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" ) ($#r1_zf_model :::"|="::: ) (Set (Set (Var "H")) ($#k6_zf_lang1 :::"/"::: ) "(" (Set (Var "y")) "," (Set (Var "x")) ")" )))))) ; theorem :: ZFMODEL2:14 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "st" (Bool (Bool (Bool "not" (Set ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H"))))) & (Bool (Set (Var "M")) "," (Set (Var "v")) ($#r1_zf_model :::"|="::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set "(" ($#k13_zf_lang :::"Ex"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) "," (Set "(" (Set (Var "H")) ($#k12_zf_lang :::"<=>"::: ) (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) ($#k4_zf_lang :::"'='"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ) ")" ")" ) ")" ")" ) ")" )) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_zf_lang1 :::"variables_in"::: ) (Set (Var "H"))))) & (Bool (Bool "not" (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H"))))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k2_zf_lang :::"x."::: ) (Num 3))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k2_zf_lang :::"x."::: ) (Num 4)))) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k2_zf_model :::"Free"::: ) (Set "(" (Set (Var "H")) ($#k6_zf_lang1 :::"/"::: ) "(" (Set (Var "y")) "," (Set (Var "x")) ")" ")" )))) & (Bool (Set (Var "M")) "," (Set (Set (Var "v")) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" ) ($#r1_zf_model :::"|="::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set "(" ($#k13_zf_lang :::"Ex"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) "," (Set "(" (Set "(" (Set (Var "H")) ($#k6_zf_lang1 :::"/"::: ) "(" (Set (Var "y")) "," (Set (Var "x")) ")" ")" ) ($#k12_zf_lang :::"<=>"::: ) (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) ($#k4_zf_lang :::"'='"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ) ")" ")" ) ")" ")" ) ")" )) & (Bool (Set ($#k1_zfmodel1 :::"def_func'"::: ) "(" (Set (Var "H")) "," (Set (Var "v")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k1_zfmodel1 :::"def_func'"::: ) "(" (Set "(" (Set (Var "H")) ($#k6_zf_lang1 :::"/"::: ) "(" (Set (Var "y")) "," (Set (Var "x")) ")" ")" ) "," (Set "(" (Set (Var "v")) ($#k2_zf_lang1 :::"/"::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" ")" ) ")" )) ")" ))))) ; theorem :: ZFMODEL2:15 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Variable":::) (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_zf_lang1 :::"variables_in"::: ) (Set (Var "H")))))) "holds" (Bool "(" (Bool (Set (Var "M")) ($#r2_zf_model :::"|="::: ) (Set (Set (Var "H")) ($#k6_zf_lang1 :::"/"::: ) "(" (Set (Var "y")) "," (Set (Var "x")) ")" )) "iff" (Bool (Set (Var "M")) ($#r2_zf_model :::"|="::: ) (Set (Var "H"))) ")" )))) ; theorem :: ZFMODEL2:16 (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "st" (Bool (Bool (Bool "not" (Set ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H1"))))) & (Bool (Set (Var "M")) "," (Set (Var "v1")) ($#r1_zf_model :::"|="::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set "(" ($#k13_zf_lang :::"Ex"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) "," (Set "(" (Set (Var "H1")) ($#k12_zf_lang :::"<=>"::: ) (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) ($#k4_zf_lang :::"'='"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ) ")" ")" ) ")" ")" ) ")" ))) "holds" (Bool "ex" (Set (Var "H2")) "being" ($#m2_finseq_1 :::"ZF-formula":::)(Bool "ex" (Set (Var "v2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "st" (Bool "(" (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set ($#k2_zf_lang :::"x."::: ) (Set (Var "j"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_zf_lang1 :::"variables_in"::: ) (Set (Var "H2")))) & (Bool (Bool "not" (Set (Var "j")) ($#r1_hidden :::"="::: ) (Num 3)))) "holds" (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Num 4)) ")" ) & (Bool (Bool "not" (Set ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H2"))))) & (Bool (Set (Var "M")) "," (Set (Var "v2")) ($#r1_zf_model :::"|="::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set "(" ($#k13_zf_lang :::"Ex"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) "," (Set "(" (Set (Var "H2")) ($#k12_zf_lang :::"<=>"::: ) (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) ($#k4_zf_lang :::"'='"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ) ")" ")" ) ")" ")" ) ")" )) & (Bool (Set ($#k1_zfmodel1 :::"def_func'"::: ) "(" (Set (Var "H1")) "," (Set (Var "v1")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k1_zfmodel1 :::"def_func'"::: ) "(" (Set (Var "H2")) "," (Set (Var "v2")) ")" )) ")" ))))))) ; theorem :: ZFMODEL2:17 (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H1")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "st" (Bool (Bool (Bool "not" (Set ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H1"))))) & (Bool (Set (Var "M")) "," (Set (Var "v1")) ($#r1_zf_model :::"|="::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set "(" ($#k13_zf_lang :::"Ex"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) "," (Set "(" (Set (Var "H1")) ($#k12_zf_lang :::"<=>"::: ) (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) ($#k4_zf_lang :::"'='"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ) ")" ")" ) ")" ")" ) ")" ))) "holds" (Bool "ex" (Set (Var "H2")) "being" ($#m2_finseq_1 :::"ZF-formula":::)(Bool "ex" (Set (Var "v2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "st" (Bool "(" (Bool (Set (Set "(" ($#k2_zf_model :::"Free"::: ) (Set (Var "H1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_zf_model :::"Free"::: ) (Set (Var "H2")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) ($#k2_tarski :::"}"::: ) )) & (Bool (Bool "not" (Set ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H2"))))) & (Bool (Set (Var "M")) "," (Set (Var "v2")) ($#r1_zf_model :::"|="::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set "(" ($#k13_zf_lang :::"Ex"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) "," (Set "(" (Set (Var "H2")) ($#k12_zf_lang :::"<=>"::: ) (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) ($#k4_zf_lang :::"'='"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ) ")" ")" ) ")" ")" ) ")" )) & (Bool (Set ($#k1_zfmodel1 :::"def_func'"::: ) "(" (Set (Var "H1")) "," (Set (Var "v1")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k1_zfmodel1 :::"def_func'"::: ) "(" (Set (Var "H2")) "," (Set (Var "v2")) ")" )) ")" )))))) ; theorem :: ZFMODEL2:18 (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F")) ($#r1_zfmodel1 :::"is_definable_in"::: ) (Set (Var "M"))) & (Bool (Set (Var "G")) ($#r1_zfmodel1 :::"is_definable_in"::: ) (Set (Var "M")))) "holds" (Bool (Set (Set (Var "F")) ($#k3_relat_1 :::"*"::: ) (Set (Var "G"))) ($#r1_zfmodel1 :::"is_definable_in"::: ) (Set (Var "M"))))) ; theorem :: ZFMODEL2:19 (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "st" (Bool (Bool (Bool "not" (Set ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H")))))) "holds" (Bool "(" (Bool (Set (Var "M")) "," (Set (Var "v")) ($#r1_zf_model :::"|="::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set "(" ($#k13_zf_lang :::"Ex"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) "," (Set "(" (Set (Var "H")) ($#k12_zf_lang :::"<=>"::: ) (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) ($#k4_zf_lang :::"'='"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ) ")" ")" ) ")" ")" ) ")" )) "iff" (Bool "for" (Set (Var "m1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "M")) (Bool "ex" (Set (Var "m2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "M")) "st" (Bool "for" (Set (Var "m3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "M")) "," (Set (Set "(" (Set (Var "v")) ($#k2_zf_lang1 :::"/"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set (Var "m1")) ")" ")" ) ($#k2_zf_lang1 :::"/"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) "," (Set (Var "m3")) ")" ) ($#r1_zf_model :::"|="::: ) (Set (Var "H"))) "iff" (Bool (Set (Var "m3")) ($#r1_hidden :::"="::: ) (Set (Var "m2"))) ")" )))) ")" )))) ; theorem :: ZFMODEL2:20 (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F")) ($#r1_zfmodel1 :::"is_definable_in"::: ) (Set (Var "M"))) & (Bool (Set (Var "G")) ($#r1_zfmodel1 :::"is_definable_in"::: ) (Set (Var "M"))) & (Bool (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool "for" (Set (Var "FG")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "FG"))) ($#r1_hidden :::"="::: ) (Set (Var "M"))) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "M")) "," (Set (Var "v")) ($#r1_zf_model :::"|="::: ) (Set (Var "H")))) "implies" (Bool (Set (Set (Var "FG")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "M")) "," (Set (Var "v")) ($#r1_zf_model :::"|="::: ) (Set ($#k6_zf_lang :::"'not'"::: ) (Set (Var "H"))))) "implies" (Bool (Set (Set (Var "FG")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "v")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) ")" ))) ")" ")" ) ")" )) "holds" (Bool (Set (Var "FG")) ($#r1_zfmodel1 :::"is_definable_in"::: ) (Set (Var "M"))))))) ; theorem :: ZFMODEL2:21 (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F")) ($#r2_zfmodel1 :::"is_parametrically_definable_in"::: ) (Set (Var "M"))) & (Bool (Set (Var "G")) ($#r2_zfmodel1 :::"is_parametrically_definable_in"::: ) (Set (Var "M")))) "holds" (Bool (Set (Set (Var "G")) ($#k3_relat_1 :::"*"::: ) (Set (Var "F"))) ($#r2_zfmodel1 :::"is_parametrically_definable_in"::: ) (Set (Var "M"))))) ; theorem :: ZFMODEL2:22 (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "," (Set (Var "H")) "being" ($#m2_finseq_1 :::"ZF-formula":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "st" (Bool (Bool (Set ($#k1_enumset1 :::"{"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) "," (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) ($#k1_enumset1 :::"}"::: ) ) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H1")))) & (Bool (Set (Var "M")) "," (Set (Var "v")) ($#r1_zf_model :::"|="::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set "(" ($#k13_zf_lang :::"Ex"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) "," (Set "(" (Set (Var "H1")) ($#k12_zf_lang :::"<=>"::: ) (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) ($#k4_zf_lang :::"'='"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ) ")" ")" ) ")" ")" ) ")" )) & (Bool (Set ($#k1_enumset1 :::"{"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) "," (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) ($#k1_enumset1 :::"}"::: ) ) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H2")))) & (Bool (Set (Var "M")) "," (Set (Var "v")) ($#r1_zf_model :::"|="::: ) (Set ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set "(" ($#k13_zf_lang :::"Ex"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k8_zf_lang :::"All"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) "," (Set "(" (Set (Var "H2")) ($#k12_zf_lang :::"<=>"::: ) (Set "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 4) ")" ) ($#k4_zf_lang :::"'='"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ")" ) ")" ")" ) ")" ")" ) ")" )) & (Bool (Set ($#k1_enumset1 :::"{"::: ) (Set "(" ($#k2_zf_lang :::"x."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 1) ")" ) "," (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 2) ")" ) ($#k1_enumset1 :::"}"::: ) ) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H")))) & (Bool (Bool "not" (Set ($#k2_zf_lang :::"x."::: ) (Num 4)) ($#r2_hidden :::"in"::: ) (Set ($#k2_zf_model :::"Free"::: ) (Set (Var "H")))))) "holds" (Bool "for" (Set (Var "FG")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "FG"))) ($#r1_hidden :::"="::: ) (Set (Var "M"))) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "M")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "M")) "," (Set (Set (Var "v")) ($#k2_zf_lang1 :::"/"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set (Var "m")) ")" ) ($#r1_zf_model :::"|="::: ) (Set (Var "H")))) "implies" (Bool (Set (Set (Var "FG")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_zfmodel1 :::"def_func'"::: ) "(" (Set (Var "H1")) "," (Set (Var "v")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "m")))) ")" & "(" (Bool (Bool (Set (Var "M")) "," (Set (Set (Var "v")) ($#k2_zf_lang1 :::"/"::: ) "(" (Set "(" ($#k2_zf_lang :::"x."::: ) (Num 3) ")" ) "," (Set (Var "m")) ")" ) ($#r1_zf_model :::"|="::: ) (Set ($#k6_zf_lang :::"'not'"::: ) (Set (Var "H"))))) "implies" (Bool (Set (Set (Var "FG")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_zfmodel1 :::"def_func'"::: ) "(" (Set (Var "H2")) "," (Set (Var "v")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "m")))) ")" ")" ) ")" )) "holds" (Bool (Set (Var "FG")) ($#r2_zfmodel1 :::"is_parametrically_definable_in"::: ) (Set (Var "M"))))))) ; theorem :: ZFMODEL2:23 (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "M"))) ($#r1_zfmodel1 :::"is_definable_in"::: ) (Set (Var "M")))) ; theorem :: ZFMODEL2:24 (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "M"))) ($#r2_zfmodel1 :::"is_parametrically_definable_in"::: ) (Set (Var "M")))) ;