:: ZF_LANG1  semantic presentation begin  































theorem :: ZF_LANG1:1 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"   (Bool  "("  (Bool (Set   ($#k18_zf_lang :::"Var1"::: )  (Set  "(" (Set (Var "x"))  ($#k4_zf_lang :::"'='"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set   ($#k19_zf_lang :::"Var2"::: )  (Set  "(" (Set (Var "x"))  ($#k4_zf_lang :::"'='"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "y")))  ")" )) ; 
 
theorem :: ZF_LANG1:2 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"   (Bool  "("  (Bool (Set   ($#k18_zf_lang :::"Var1"::: )  (Set  "(" (Set (Var "x"))  ($#k5_zf_lang :::"'in'"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set   ($#k19_zf_lang :::"Var2"::: )  (Set  "(" (Set (Var "x"))  ($#k5_zf_lang :::"'in'"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "y")))  ")" )) ; 
 
theorem :: ZF_LANG1:3 (Bool  "for" (Set (Var "p")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) "holds"  (Bool (Set   ($#k20_zf_lang :::"the_argument_of"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "p")))) ; 
 
theorem :: ZF_LANG1:4 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) "holds"   (Bool  "("  (Bool (Set   ($#k21_zf_lang :::"the_left_argument_of"::: )  (Set  "(" (Set (Var "p"))  ($#k7_zf_lang :::"'&'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "p"))) & (Bool (Set   ($#k22_zf_lang :::"the_right_argument_of"::: )  (Set  "(" (Set (Var "p"))  ($#k7_zf_lang :::"'&'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "q")))  ")" )) ; 
 
theorem :: ZF_LANG1:5 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) "holds"   (Bool  "("  (Bool (Set   ($#k21_zf_lang :::"the_left_argument_of"::: )  (Set  "(" (Set (Var "p"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "p"))) & (Bool (Set   ($#k22_zf_lang :::"the_right_argument_of"::: )  (Set  "(" (Set (Var "p"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "q")))  ")" )) ; 
 
theorem :: ZF_LANG1:6 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) "holds"   (Bool  "("  (Bool (Set   ($#k25_zf_lang :::"the_antecedent_of"::: )  (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "p"))) & (Bool (Set   ($#k26_zf_lang :::"the_consequent_of"::: )  (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "q")))  ")" )) ; 
 
theorem :: ZF_LANG1:7 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) "holds"   (Bool  "("  (Bool (Set   ($#k27_zf_lang :::"the_left_side_of"::: )  (Set  "(" (Set (Var "p"))  ($#k12_zf_lang :::"<=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "p"))) & (Bool (Set   ($#k28_zf_lang :::"the_right_side_of"::: )  (Set  "(" (Set (Var "p"))  ($#k12_zf_lang :::"<=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "q")))  ")" )) ; 
 
theorem :: ZF_LANG1:8 (Bool  "for" (Set (Var "p")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"   (Bool  "("  (Bool (Set   ($#k23_zf_lang :::"bound_in"::: )  (Set  "("  ($#k8_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "p")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set   ($#k24_zf_lang :::"the_scope_of"::: )  (Set  "("  ($#k8_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "p")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "p")))  ")" ))) ; 
 
theorem :: ZF_LANG1:9 (Bool  "for" (Set (Var "p")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"   (Bool  "("  (Bool (Set   ($#k23_zf_lang :::"bound_in"::: )  (Set  "("  ($#k13_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "p")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set   ($#k24_zf_lang :::"the_scope_of"::: )  (Set  "("  ($#k13_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "p")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "p")))  ")" ))) ; 
 
theorem :: ZF_LANG1:10 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) "holds"  (Bool (Set (Set (Var "p"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set (Var "q"))))) ; 
 
theorem :: ZF_LANG1:11 (Bool  "for" (Set (Var "p")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"   (Bool  "("  (Bool (Set   ($#k14_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "p")) ")" ) "is"   ($#v6_zf_lang :::"universal"::: )  ) & (Bool (Set   ($#k23_zf_lang :::"bound_in"::: )  (Set  "("  ($#k14_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "p")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set   ($#k24_zf_lang :::"the_scope_of"::: )  (Set  "("  ($#k14_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "p")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k8_zf_lang :::"All"::: )   "(" (Set (Var "y")) "," (Set (Var "p")) ")" ))  ")" ))) ; 
 
theorem :: ZF_LANG1:12 (Bool  "for" (Set (Var "p")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"   (Bool  "("  (Bool (Set   ($#k15_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "p")) ")" ) "is"   ($#v11_zf_lang :::"existential"::: )  ) & (Bool (Set   ($#k23_zf_lang :::"bound_in"::: )  (Set  "("  ($#k15_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "p")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set   ($#k24_zf_lang :::"the_scope_of"::: )  (Set  "("  ($#k15_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "p")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k13_zf_lang :::"Ex"::: )   "(" (Set (Var "y")) "," (Set (Var "p")) ")" ))  ")" ))) ; 
 
theorem :: ZF_LANG1:13 (Bool  "for" (Set (Var "p")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"   (Bool  "("  (Bool (Set   ($#k16_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set  "("  ($#k8_zf_lang :::"All"::: )   "(" (Set (Var "y")) "," (Set  "("  ($#k8_zf_lang :::"All"::: )   "(" (Set (Var "z")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" )) & (Bool (Set   ($#k16_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k14_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set  "("  ($#k8_zf_lang :::"All"::: )   "(" (Set (Var "z")) "," (Set (Var "p")) ")"  ")" ) ")" ))  ")" ))) ; 
 
theorem :: ZF_LANG1:14 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "being"   ($#m2_subset_1 :::"Variable":::)  "st" (Bool (Bool (Set   ($#k14_zf_lang :::"All"::: )   "(" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "p1")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k14_zf_lang :::"All"::: )   "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "p2")) ")" ))) "holds"  (Bool  "("  (Bool (Set (Var "x1"))  ($#r1_hidden :::"="::: )  (Set (Var "x2"))) & (Bool (Set (Var "y1"))  ($#r1_hidden :::"="::: )  (Set (Var "y2"))) & (Bool (Set (Var "p1"))  ($#r1_hidden :::"="::: )  (Set (Var "p2")))  ")" ))) ; 
 
theorem :: ZF_LANG1:15 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "z1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "z2")) "being"   ($#m2_subset_1 :::"Variable":::)  "st" (Bool (Bool (Set   ($#k16_zf_lang :::"All"::: )   "(" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "z1")) "," (Set (Var "p1")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k16_zf_lang :::"All"::: )   "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "z2")) "," (Set (Var "p2")) ")" ))) "holds"  (Bool  "("  (Bool (Set (Var "x1"))  ($#r1_hidden :::"="::: )  (Set (Var "x2"))) & (Bool (Set (Var "y1"))  ($#r1_hidden :::"="::: )  (Set (Var "y2"))) & (Bool (Set (Var "z1"))  ($#r1_hidden :::"="::: )  (Set (Var "z2"))) & (Bool (Set (Var "p1"))  ($#r1_hidden :::"="::: )  (Set (Var "p2")))  ")" ))) ; 
 
theorem :: ZF_LANG1:16 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "," (Set (Var "s")) "being"   ($#m2_subset_1 :::"Variable":::)  "st" (Bool (Bool (Set   ($#k16_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k14_zf_lang :::"All"::: )   "(" (Set (Var "t")) "," (Set (Var "s")) "," (Set (Var "q")) ")" ))) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "t"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "s"))) & (Bool (Set   ($#k8_zf_lang :::"All"::: )   "(" (Set (Var "z")) "," (Set (Var "p")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "q")))  ")" ))) ; 
 
theorem :: ZF_LANG1:17 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "being"   ($#m2_subset_1 :::"Variable":::)  "st" (Bool (Bool (Set   ($#k15_zf_lang :::"Ex"::: )   "(" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "p1")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k15_zf_lang :::"Ex"::: )   "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "p2")) ")" ))) "holds"  (Bool  "("  (Bool (Set (Var "x1"))  ($#r1_hidden :::"="::: )  (Set (Var "x2"))) & (Bool (Set (Var "y1"))  ($#r1_hidden :::"="::: )  (Set (Var "y2"))) & (Bool (Set (Var "p1"))  ($#r1_hidden :::"="::: )  (Set (Var "p2")))  ")" ))) ; 
 
theorem :: ZF_LANG1:18 (Bool  "for" (Set (Var "p")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"   (Bool  "("  (Bool (Set   ($#k17_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k13_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set  "("  ($#k13_zf_lang :::"Ex"::: )   "(" (Set (Var "y")) "," (Set  "("  ($#k13_zf_lang :::"Ex"::: )   "(" (Set (Var "z")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" )) & (Bool (Set   ($#k17_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k15_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set  "("  ($#k13_zf_lang :::"Ex"::: )   "(" (Set (Var "z")) "," (Set (Var "p")) ")"  ")" ) ")" ))  ")" ))) ; 
 
theorem :: ZF_LANG1:19 (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "z1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "z2")) "being"   ($#m2_subset_1 :::"Variable":::)  "st" (Bool (Bool (Set   ($#k17_zf_lang :::"Ex"::: )   "(" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "z1")) "," (Set (Var "p1")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k17_zf_lang :::"Ex"::: )   "(" (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "z2")) "," (Set (Var "p2")) ")" ))) "holds"  (Bool  "("  (Bool (Set (Var "x1"))  ($#r1_hidden :::"="::: )  (Set (Var "x2"))) & (Bool (Set (Var "y1"))  ($#r1_hidden :::"="::: )  (Set (Var "y2"))) & (Bool (Set (Var "z1"))  ($#r1_hidden :::"="::: )  (Set (Var "z2"))) & (Bool (Set (Var "p1"))  ($#r1_hidden :::"="::: )  (Set (Var "p2")))  ")" ))) ; 
 
theorem :: ZF_LANG1:20 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "," (Set (Var "s")) "being"   ($#m2_subset_1 :::"Variable":::)  "st" (Bool (Bool (Set   ($#k17_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k15_zf_lang :::"Ex"::: )   "(" (Set (Var "t")) "," (Set (Var "s")) "," (Set (Var "q")) ")" ))) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "t"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "s"))) & (Bool (Set   ($#k13_zf_lang :::"Ex"::: )   "(" (Set (Var "z")) "," (Set (Var "p")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "q")))  ")" ))) ; 
 
theorem :: ZF_LANG1:21 (Bool  "for" (Set (Var "p")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"   (Bool  "("  (Bool (Set   ($#k16_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")" ) "is"   ($#v6_zf_lang :::"universal"::: )  ) & (Bool (Set   ($#k23_zf_lang :::"bound_in"::: )  (Set  "("  ($#k16_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set   ($#k24_zf_lang :::"the_scope_of"::: )  (Set  "("  ($#k16_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k14_zf_lang :::"All"::: )   "(" (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")" ))  ")" ))) ; 
 
theorem :: ZF_LANG1:22 (Bool  "for" (Set (Var "p")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"   (Bool  "("  (Bool (Set   ($#k17_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")" ) "is"   ($#v11_zf_lang :::"existential"::: )  ) & (Bool (Set   ($#k23_zf_lang :::"bound_in"::: )  (Set  "("  ($#k17_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set   ($#k24_zf_lang :::"the_scope_of"::: )  (Set  "("  ($#k17_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k15_zf_lang :::"Ex"::: )   "(" (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")" ))  ")" ))) ; 
 
theorem :: ZF_LANG1:23 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  "st" (Bool (Bool (Set (Var "H")) "is"   ($#v8_zf_lang :::"disjunctive"::: )  )) "holds"  (Bool (Set   ($#k21_zf_lang :::"the_left_argument_of"::: )  (Set (Var "H")))  ($#r1_hidden :::"="::: )  (Set   ($#k20_zf_lang :::"the_argument_of"::: )  (Set  "("  ($#k21_zf_lang :::"the_left_argument_of"::: )  (Set  "("  ($#k20_zf_lang :::"the_argument_of"::: )  (Set (Var "H")) ")" ) ")" )))) ; 
 
theorem :: ZF_LANG1:24 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  "st" (Bool (Bool (Set (Var "H")) "is"   ($#v8_zf_lang :::"disjunctive"::: )  )) "holds"  (Bool (Set   ($#k22_zf_lang :::"the_right_argument_of"::: )  (Set (Var "H")))  ($#r1_hidden :::"="::: )  (Set   ($#k20_zf_lang :::"the_argument_of"::: )  (Set  "("  ($#k22_zf_lang :::"the_right_argument_of"::: )  (Set  "("  ($#k20_zf_lang :::"the_argument_of"::: )  (Set (Var "H")) ")" ) ")" )))) ; 
 
theorem :: ZF_LANG1:25 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  "st" (Bool (Bool (Set (Var "H")) "is"   ($#v9_zf_lang :::"conditional"::: )  )) "holds"  (Bool (Set   ($#k25_zf_lang :::"the_antecedent_of"::: )  (Set (Var "H")))  ($#r1_hidden :::"="::: )  (Set   ($#k21_zf_lang :::"the_left_argument_of"::: )  (Set  "("  ($#k20_zf_lang :::"the_argument_of"::: )  (Set (Var "H")) ")" )))) ; 
 
theorem :: ZF_LANG1:26 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  "st" (Bool (Bool (Set (Var "H")) "is"   ($#v9_zf_lang :::"conditional"::: )  )) "holds"  (Bool (Set   ($#k26_zf_lang :::"the_consequent_of"::: )  (Set (Var "H")))  ($#r1_hidden :::"="::: )  (Set   ($#k20_zf_lang :::"the_argument_of"::: )  (Set  "("  ($#k22_zf_lang :::"the_right_argument_of"::: )  (Set  "("  ($#k20_zf_lang :::"the_argument_of"::: )  (Set (Var "H")) ")" ) ")" )))) ; 
 
theorem :: ZF_LANG1:27 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  "st" (Bool (Bool (Set (Var "H")) "is"   ($#v10_zf_lang :::"biconditional"::: )  )) "holds"  (Bool  "("  (Bool (Set   ($#k27_zf_lang :::"the_left_side_of"::: )  (Set (Var "H")))  ($#r1_hidden :::"="::: )  (Set   ($#k25_zf_lang :::"the_antecedent_of"::: )  (Set  "("  ($#k21_zf_lang :::"the_left_argument_of"::: )  (Set (Var "H")) ")" ))) & (Bool (Set   ($#k27_zf_lang :::"the_left_side_of"::: )  (Set (Var "H")))  ($#r1_hidden :::"="::: )  (Set   ($#k26_zf_lang :::"the_consequent_of"::: )  (Set  "("  ($#k22_zf_lang :::"the_right_argument_of"::: )  (Set (Var "H")) ")" )))  ")" )) ; 
 
theorem :: ZF_LANG1:28 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  "st" (Bool (Bool (Set (Var "H")) "is"   ($#v10_zf_lang :::"biconditional"::: )  )) "holds"  (Bool  "("  (Bool (Set   ($#k28_zf_lang :::"the_right_side_of"::: )  (Set (Var "H")))  ($#r1_hidden :::"="::: )  (Set   ($#k26_zf_lang :::"the_consequent_of"::: )  (Set  "("  ($#k21_zf_lang :::"the_left_argument_of"::: )  (Set (Var "H")) ")" ))) & (Bool (Set   ($#k28_zf_lang :::"the_right_side_of"::: )  (Set (Var "H")))  ($#r1_hidden :::"="::: )  (Set   ($#k25_zf_lang :::"the_antecedent_of"::: )  (Set  "("  ($#k22_zf_lang :::"the_right_argument_of"::: )  (Set (Var "H")) ")" )))  ")" )) ; 
 
theorem :: ZF_LANG1:29 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  "st" (Bool (Bool (Set (Var "H")) "is"   ($#v11_zf_lang :::"existential"::: )  )) "holds"  (Bool  "("  (Bool (Set   ($#k23_zf_lang :::"bound_in"::: )  (Set (Var "H")))  ($#r1_hidden :::"="::: )  (Set   ($#k23_zf_lang :::"bound_in"::: )  (Set  "("  ($#k20_zf_lang :::"the_argument_of"::: )  (Set (Var "H")) ")" ))) & (Bool (Set   ($#k24_zf_lang :::"the_scope_of"::: )  (Set (Var "H")))  ($#r1_hidden :::"="::: )  (Set   ($#k20_zf_lang :::"the_argument_of"::: )  (Set  "("  ($#k24_zf_lang :::"the_scope_of"::: )  (Set  "("  ($#k20_zf_lang :::"the_argument_of"::: )  (Set (Var "H")) ")" ) ")" )))  ")" )) ; 
 
theorem :: ZF_LANG1:30 (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) "holds"   (Bool  "("  (Bool (Set   ($#k20_zf_lang :::"the_argument_of"::: )  (Set  "(" (Set (Var "F"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "G")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "F")) ")" )  ($#k7_zf_lang :::"'&'"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "G")) ")" ))) & (Bool (Set   ($#k25_zf_lang :::"the_antecedent_of"::: )  (Set  "(" (Set (Var "F"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "G")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_zf_lang :::"'not'"::: )  (Set (Var "F")))) & (Bool (Set   ($#k26_zf_lang :::"the_consequent_of"::: )  (Set  "(" (Set (Var "F"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "G")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "G")))  ")" )) ; 
 
theorem :: ZF_LANG1:31 (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) "holds"  (Bool (Set   ($#k20_zf_lang :::"the_argument_of"::: )  (Set  "(" (Set (Var "F"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "G")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k7_zf_lang :::"'&'"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "G")) ")" )))) ; 
 
theorem :: ZF_LANG1:32 (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) "holds"   (Bool  "("  (Bool (Set   ($#k21_zf_lang :::"the_left_argument_of"::: )  (Set  "(" (Set (Var "F"))  ($#k12_zf_lang :::"<=>"::: )  (Set (Var "G")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "G")))) & (Bool (Set   ($#k22_zf_lang :::"the_right_argument_of"::: )  (Set  "(" (Set (Var "F"))  ($#k12_zf_lang :::"<=>"::: )  (Set (Var "G")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "F"))))  ")" )) ; 
 
theorem :: ZF_LANG1:33 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"  (Bool (Set   ($#k20_zf_lang :::"the_argument_of"::: )  (Set  "("  ($#k13_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "H")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k8_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "H")) ")" ) ")" )))) ; 
 
theorem :: ZF_LANG1:34 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  "st" (Bool (Bool (Set (Var "H")) "is"   ($#v8_zf_lang :::"disjunctive"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "H")) "is"   ($#v9_zf_lang :::"conditional"::: )  ) & (Bool (Set (Var "H")) "is"   ($#v4_zf_lang :::"negative"::: )  ) & (Bool (Set   ($#k20_zf_lang :::"the_argument_of"::: )  (Set (Var "H"))) "is"   ($#v5_zf_lang :::"conjunctive"::: )  ) & (Bool (Set   ($#k21_zf_lang :::"the_left_argument_of"::: )  (Set  "("  ($#k20_zf_lang :::"the_argument_of"::: )  (Set (Var "H")) ")" )) "is"   ($#v4_zf_lang :::"negative"::: )  ) & (Bool (Set   ($#k22_zf_lang :::"the_right_argument_of"::: )  (Set  "("  ($#k20_zf_lang :::"the_argument_of"::: )  (Set (Var "H")) ")" )) "is"   ($#v4_zf_lang :::"negative"::: )  )  ")" )) ; 
 
theorem :: ZF_LANG1:35 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  "st" (Bool (Bool (Set (Var "H")) "is"   ($#v9_zf_lang :::"conditional"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "H")) "is"   ($#v4_zf_lang :::"negative"::: )  ) & (Bool (Set   ($#k20_zf_lang :::"the_argument_of"::: )  (Set (Var "H"))) "is"   ($#v5_zf_lang :::"conjunctive"::: )  ) & (Bool (Set   ($#k22_zf_lang :::"the_right_argument_of"::: )  (Set  "("  ($#k20_zf_lang :::"the_argument_of"::: )  (Set (Var "H")) ")" )) "is"   ($#v4_zf_lang :::"negative"::: )  )  ")" )) ; 
 
theorem :: ZF_LANG1:36 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  "st" (Bool (Bool (Set (Var "H")) "is"   ($#v10_zf_lang :::"biconditional"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "H")) "is"   ($#v5_zf_lang :::"conjunctive"::: )  ) & (Bool (Set   ($#k21_zf_lang :::"the_left_argument_of"::: )  (Set (Var "H"))) "is"   ($#v9_zf_lang :::"conditional"::: )  ) & (Bool (Set   ($#k22_zf_lang :::"the_right_argument_of"::: )  (Set (Var "H"))) "is"   ($#v9_zf_lang :::"conditional"::: )  )  ")" )) ; 
 
theorem :: ZF_LANG1:37 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  "st" (Bool (Bool (Set (Var "H")) "is"   ($#v11_zf_lang :::"existential"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "H")) "is"   ($#v4_zf_lang :::"negative"::: )  ) & (Bool (Set   ($#k20_zf_lang :::"the_argument_of"::: )  (Set (Var "H"))) "is"   ($#v6_zf_lang :::"universal"::: )  ) & (Bool (Set   ($#k24_zf_lang :::"the_scope_of"::: )  (Set  "("  ($#k20_zf_lang :::"the_argument_of"::: )  (Set (Var "H")) ")" )) "is"   ($#v4_zf_lang :::"negative"::: )  )  ")" )) ; 
 
theorem :: ZF_LANG1:38 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) "holds"   (Bool  "("  (Bool  "("   "not" (Bool (Set (Var "H")) "is"   ($#v2_zf_lang :::"being_equality"::: )  ) "or" (Bool  "("  (Bool (Bool  "not" (Set (Var "H")) "is"   ($#v3_zf_lang :::"being_membership"::: )  )) & (Bool (Bool  "not" (Set (Var "H")) "is"   ($#v4_zf_lang :::"negative"::: )  )) & (Bool (Bool  "not" (Set (Var "H")) "is"   ($#v5_zf_lang :::"conjunctive"::: )  )) & (Bool (Bool  "not" (Set (Var "H")) "is"   ($#v6_zf_lang :::"universal"::: )  ))  ")" )  ")" ) & (Bool  "("   "not" (Bool (Set (Var "H")) "is"   ($#v3_zf_lang :::"being_membership"::: )  ) "or" (Bool  "("  (Bool (Bool  "not" (Set (Var "H")) "is"   ($#v4_zf_lang :::"negative"::: )  )) & (Bool (Bool  "not" (Set (Var "H")) "is"   ($#v5_zf_lang :::"conjunctive"::: )  )) & (Bool (Bool  "not" (Set (Var "H")) "is"   ($#v6_zf_lang :::"universal"::: )  ))  ")" )  ")" ) & (Bool  "("   "not" (Bool (Set (Var "H")) "is"   ($#v4_zf_lang :::"negative"::: )  ) "or" (Bool  "("  (Bool (Bool  "not" (Set (Var "H")) "is"   ($#v5_zf_lang :::"conjunctive"::: )  )) & (Bool (Bool  "not" (Set (Var "H")) "is"   ($#v6_zf_lang :::"universal"::: )  ))  ")" )  ")" ) & (Bool  "("   "not" (Bool (Set (Var "H")) "is"   ($#v5_zf_lang :::"conjunctive"::: )  ) "or"  "not" (Bool (Set (Var "H")) "is"   ($#v6_zf_lang :::"universal"::: )  )  ")" )  ")" )) ; 
 
theorem :: ZF_LANG1:39 (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  "st" (Bool (Bool (Set (Var "F"))  ($#r2_zf_lang :::"is_subformula_of"::: )  (Set (Var "G")))) "holds"  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "F")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "G"))))) ; 
 
theorem :: ZF_LANG1:40 (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  "st" (Bool (Bool  "("  (Bool  "("  (Bool (Set (Var "F"))  ($#r3_zf_lang :::"is_proper_subformula_of"::: )  (Set (Var "G"))) & (Bool (Set (Var "G"))  ($#r2_zf_lang :::"is_subformula_of"::: )  (Set (Var "H")))  ")" ) "or" (Bool  "("  (Bool (Set (Var "F"))  ($#r2_zf_lang :::"is_subformula_of"::: )  (Set (Var "G"))) & (Bool (Set (Var "G"))  ($#r3_zf_lang :::"is_proper_subformula_of"::: )  (Set (Var "H")))  ")" ) "or" (Bool  "("  (Bool (Set (Var "F"))  ($#r2_zf_lang :::"is_subformula_of"::: )  (Set (Var "G"))) & (Bool (Set (Var "G"))  ($#r1_zf_lang :::"is_immediate_constituent_of"::: )  (Set (Var "H")))  ")" ) "or" (Bool  "("  (Bool (Set (Var "F"))  ($#r1_zf_lang :::"is_immediate_constituent_of"::: )  (Set (Var "G"))) & (Bool (Set (Var "G"))  ($#r2_zf_lang :::"is_subformula_of"::: )  (Set (Var "H")))  ")" ) "or" (Bool  "("  (Bool (Set (Var "F"))  ($#r3_zf_lang :::"is_proper_subformula_of"::: )  (Set (Var "G"))) & (Bool (Set (Var "G"))  ($#r1_zf_lang :::"is_immediate_constituent_of"::: )  (Set (Var "H")))  ")" ) "or" (Bool  "("  (Bool (Set (Var "F"))  ($#r1_zf_lang :::"is_immediate_constituent_of"::: )  (Set (Var "G"))) & (Bool (Set (Var "G"))  ($#r3_zf_lang :::"is_proper_subformula_of"::: )  (Set (Var "H")))  ")" )  ")" )) "holds"  (Bool (Set (Var "F"))  ($#r3_zf_lang :::"is_proper_subformula_of"::: )  (Set (Var "H")))) ; 
 
theorem :: ZF_LANG1:41 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  "holds" (Bool (Bool  "not" (Set (Var "H"))  ($#r1_zf_lang :::"is_immediate_constituent_of"::: )  (Set (Var "H"))))) ; 
 
theorem :: ZF_LANG1:42 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "G"))  ($#r3_zf_lang :::"is_proper_subformula_of"::: )  (Set (Var "H"))) "or"  "not" (Bool (Set (Var "H"))  ($#r2_zf_lang :::"is_subformula_of"::: )  (Set (Var "G")))  ")" )) ; 
 
theorem :: ZF_LANG1:43 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "G"))  ($#r3_zf_lang :::"is_proper_subformula_of"::: )  (Set (Var "H"))) "or"  "not" (Bool (Set (Var "H"))  ($#r3_zf_lang :::"is_proper_subformula_of"::: )  (Set (Var "G")))  ")" )) ; 
 
theorem :: ZF_LANG1:44 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "G"))  ($#r2_zf_lang :::"is_subformula_of"::: )  (Set (Var "H"))) "or"  "not" (Bool (Set (Var "H"))  ($#r1_zf_lang :::"is_immediate_constituent_of"::: )  (Set (Var "G")))  ")" )) ; 
 
theorem :: ZF_LANG1:45 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  "holds"  (Bool  "("   "not" (Bool (Set (Var "G"))  ($#r3_zf_lang :::"is_proper_subformula_of"::: )  (Set (Var "H"))) "or"  "not" (Bool (Set (Var "H"))  ($#r1_zf_lang :::"is_immediate_constituent_of"::: )  (Set (Var "G")))  ")" )) ; 
 
theorem :: ZF_LANG1:46 (Bool  "for" (Set (Var "F")) "," (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  "st" (Bool (Bool (Set   ($#k6_zf_lang :::"'not'"::: )  (Set (Var "F")))  ($#r2_zf_lang :::"is_subformula_of"::: )  (Set (Var "H")))) "holds"  (Bool (Set (Var "F"))  ($#r3_zf_lang :::"is_proper_subformula_of"::: )  (Set (Var "H")))) ; 
 
theorem :: ZF_LANG1:47 (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  "st" (Bool (Bool (Set (Set (Var "F"))  ($#k7_zf_lang :::"'&'"::: )  (Set (Var "G")))  ($#r2_zf_lang :::"is_subformula_of"::: )  (Set (Var "H")))) "holds"  (Bool  "("  (Bool (Set (Var "F"))  ($#r3_zf_lang :::"is_proper_subformula_of"::: )  (Set (Var "H"))) & (Bool (Set (Var "G"))  ($#r3_zf_lang :::"is_proper_subformula_of"::: )  (Set (Var "H")))  ")" )) ; 
 
theorem :: ZF_LANG1:48 (Bool  "for" (Set (Var "H")) "," (Set (Var "F")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m2_subset_1 :::"Variable":::)  "st" (Bool (Bool (Set   ($#k8_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "H")) ")" )  ($#r2_zf_lang :::"is_subformula_of"::: )  (Set (Var "F")))) "holds"  (Bool (Set (Var "H"))  ($#r3_zf_lang :::"is_proper_subformula_of"::: )  (Set (Var "F"))))) ; 
 
theorem :: ZF_LANG1:49 (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) "holds"   (Bool  "("  (Bool (Set (Set (Var "F"))  ($#k7_zf_lang :::"'&'"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "G")) ")" ))  ($#r3_zf_lang :::"is_proper_subformula_of"::: )  (Set (Set (Var "F"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "G")))) & (Bool (Set (Var "F"))  ($#r3_zf_lang :::"is_proper_subformula_of"::: )  (Set (Set (Var "F"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "G")))) & (Bool (Set   ($#k6_zf_lang :::"'not'"::: )  (Set (Var "G")))  ($#r3_zf_lang :::"is_proper_subformula_of"::: )  (Set (Set (Var "F"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "G")))) & (Bool (Set (Var "G"))  ($#r3_zf_lang :::"is_proper_subformula_of"::: )  (Set (Set (Var "F"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "G"))))  ")" )) ; 
 
theorem :: ZF_LANG1:50 (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "F")) ")" )  ($#k7_zf_lang :::"'&'"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "G")) ")" ))  ($#r3_zf_lang :::"is_proper_subformula_of"::: )  (Set (Set (Var "F"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "G")))) & (Bool (Set   ($#k6_zf_lang :::"'not'"::: )  (Set (Var "F")))  ($#r3_zf_lang :::"is_proper_subformula_of"::: )  (Set (Set (Var "F"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "G")))) & (Bool (Set   ($#k6_zf_lang :::"'not'"::: )  (Set (Var "G")))  ($#r3_zf_lang :::"is_proper_subformula_of"::: )  (Set (Set (Var "F"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "G")))) & (Bool (Set (Var "F"))  ($#r3_zf_lang :::"is_proper_subformula_of"::: )  (Set (Set (Var "F"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "G")))) & (Bool (Set (Var "G"))  ($#r3_zf_lang :::"is_proper_subformula_of"::: )  (Set (Set (Var "F"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "G"))))  ")" )) ; 
 
theorem :: ZF_LANG1:51 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"   (Bool  "("  (Bool (Set   ($#k8_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "H")) ")" ) ")" )  ($#r3_zf_lang :::"is_proper_subformula_of"::: )  (Set   ($#k13_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "H")) ")" )) & (Bool (Set   ($#k6_zf_lang :::"'not'"::: )  (Set (Var "H")))  ($#r3_zf_lang :::"is_proper_subformula_of"::: )  (Set   ($#k13_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "H")) ")" ))  ")" ))) ; 
 
theorem :: ZF_LANG1:52 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) "holds"   (Bool  "("  (Bool (Set (Var "G"))  ($#r2_zf_lang :::"is_subformula_of"::: )  (Set (Var "H"))) "iff" (Bool (Set (Var "G"))  ($#r2_hidden :::"in"::: )  (Set   ($#k29_zf_lang :::"Subformulae"::: )  (Set (Var "H"))))  ")" )) ; 
 
theorem :: ZF_LANG1:53 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  "st" (Bool (Bool (Set (Var "G"))  ($#r2_hidden :::"in"::: )  (Set   ($#k29_zf_lang :::"Subformulae"::: )  (Set (Var "H"))))) "holds"  (Bool (Set   ($#k29_zf_lang :::"Subformulae"::: )  (Set (Var "G")))  ($#r1_tarski :::"c="::: )  (Set   ($#k29_zf_lang :::"Subformulae"::: )  (Set (Var "H"))))) ; 
 
theorem :: ZF_LANG1:54 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) "holds"  (Bool (Set (Var "H"))  ($#r2_hidden :::"in"::: )  (Set   ($#k29_zf_lang :::"Subformulae"::: )  (Set (Var "H"))))) ; 
 
theorem :: ZF_LANG1:55 (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) "holds"  (Bool (Set   ($#k29_zf_lang :::"Subformulae"::: )  (Set  "(" (Set (Var "F"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "G")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k29_zf_lang :::"Subformulae"::: )  (Set (Var "F")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "("  ($#k29_zf_lang :::"Subformulae"::: )  (Set (Var "G")) ")" ) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_enumset1 :::"{"::: ) (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "G")) ")" ) "," (Set  "(" (Set (Var "F"))  ($#k7_zf_lang :::"'&'"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "G")) ")" ) ")" ) "," (Set  "(" (Set (Var "F"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "G")) ")" ) ($#k1_enumset1 :::"}"::: ) )))) ; 
 
theorem :: ZF_LANG1:56 (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) "holds"  (Bool (Set   ($#k29_zf_lang :::"Subformulae"::: )  (Set  "(" (Set (Var "F"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "G")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k29_zf_lang :::"Subformulae"::: )  (Set (Var "F")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "("  ($#k29_zf_lang :::"Subformulae"::: )  (Set (Var "G")) ")" ) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_enumset1 :::"{"::: ) (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "G")) ")" ) "," (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "F")) ")" ) "," (Set  "(" (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "F")) ")" )  ($#k7_zf_lang :::"'&'"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "G")) ")" ) ")" ) "," (Set  "(" (Set (Var "F"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "G")) ")" ) ($#k2_enumset1 :::"}"::: ) )))) ; 
 
theorem :: ZF_LANG1:57 (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) "holds"  (Bool (Set   ($#k29_zf_lang :::"Subformulae"::: )  (Set  "(" (Set (Var "F"))  ($#k12_zf_lang :::"<=>"::: )  (Set (Var "G")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k29_zf_lang :::"Subformulae"::: )  (Set (Var "F")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "("  ($#k29_zf_lang :::"Subformulae"::: )  (Set (Var "G")) ")" ) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k5_enumset1 :::"{"::: ) (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "G")) ")" ) "," (Set  "(" (Set (Var "F"))  ($#k7_zf_lang :::"'&'"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "G")) ")" ) ")" ) "," (Set  "(" (Set (Var "F"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "G")) ")" ) "," (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "F")) ")" ) "," (Set  "(" (Set (Var "G"))  ($#k7_zf_lang :::"'&'"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "F")) ")" ) ")" ) "," (Set  "(" (Set (Var "G"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "F")) ")" ) "," (Set  "(" (Set (Var "F"))  ($#k12_zf_lang :::"<=>"::: )  (Set (Var "G")) ")" ) ($#k5_enumset1 :::"}"::: ) )))) ; 
 
theorem :: ZF_LANG1:58 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"  (Bool (Set   ($#k2_zf_model :::"Free"::: )  (Set  "(" (Set (Var "x"))  ($#k4_zf_lang :::"'='"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ))) ; 
 
theorem :: ZF_LANG1:59 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"  (Bool (Set   ($#k2_zf_model :::"Free"::: )  (Set  "(" (Set (Var "x"))  ($#k5_zf_lang :::"'in'"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ))) ; 
 
theorem :: ZF_LANG1:60 (Bool  "for" (Set (Var "p")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) "holds"  (Bool (Set   ($#k2_zf_model :::"Free"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_zf_model :::"Free"::: )  (Set (Var "p"))))) ; 
 
theorem :: ZF_LANG1:61 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) "holds"  (Bool (Set   ($#k2_zf_model :::"Free"::: )  (Set  "(" (Set (Var "p"))  ($#k7_zf_lang :::"'&'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_zf_model :::"Free"::: )  (Set (Var "p")) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_zf_model :::"Free"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: ZF_LANG1:62 (Bool  "for" (Set (Var "p")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"  (Bool (Set   ($#k2_zf_model :::"Free"::: )  (Set  "("  ($#k8_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "p")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_zf_model :::"Free"::: )  (Set (Var "p")) ")" )  ($#k7_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))))) ; 
 
theorem :: ZF_LANG1:63 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) "holds"  (Bool (Set   ($#k2_zf_model :::"Free"::: )  (Set  "(" (Set (Var "p"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_zf_model :::"Free"::: )  (Set (Var "p")) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_zf_model :::"Free"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: ZF_LANG1:64 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) "holds"  (Bool (Set   ($#k2_zf_model :::"Free"::: )  (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_zf_model :::"Free"::: )  (Set (Var "p")) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_zf_model :::"Free"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: ZF_LANG1:65 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) "holds"  (Bool (Set   ($#k2_zf_model :::"Free"::: )  (Set  "(" (Set (Var "p"))  ($#k12_zf_lang :::"<=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_zf_model :::"Free"::: )  (Set (Var "p")) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_zf_model :::"Free"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: ZF_LANG1:66 (Bool  "for" (Set (Var "p")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"  (Bool (Set   ($#k2_zf_model :::"Free"::: )  (Set  "("  ($#k13_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "p")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_zf_model :::"Free"::: )  (Set (Var "p")) ")" )  ($#k7_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))))) ; 
 
theorem :: ZF_LANG1:67 (Bool  "for" (Set (Var "p")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"  (Bool (Set   ($#k2_zf_model :::"Free"::: )  (Set  "("  ($#k14_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "p")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_zf_model :::"Free"::: )  (Set (Var "p")) ")" )  ($#k7_subset_1 :::"\"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ))))) ; 
 
theorem :: ZF_LANG1:68 (Bool  "for" (Set (Var "p")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"  (Bool (Set   ($#k2_zf_model :::"Free"::: )  (Set  "("  ($#k16_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_zf_model :::"Free"::: )  (Set (Var "p")) ")" )  ($#k7_subset_1 :::"\"::: )  (Set  ($#k1_enumset1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k1_enumset1 :::"}"::: ) ))))) ; 
 
theorem :: ZF_LANG1:69 (Bool  "for" (Set (Var "p")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"  (Bool (Set   ($#k2_zf_model :::"Free"::: )  (Set  "("  ($#k15_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "p")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_zf_model :::"Free"::: )  (Set (Var "p")) ")" )  ($#k7_subset_1 :::"\"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ))))) ; 
 
theorem :: ZF_LANG1:70 (Bool  "for" (Set (Var "p")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"  (Bool (Set   ($#k2_zf_model :::"Free"::: )  (Set  "("  ($#k17_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "p")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_zf_model :::"Free"::: )  (Set (Var "p")) ")" )  ($#k7_subset_1 :::"\"::: )  (Set  ($#k1_enumset1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k1_enumset1 :::"}"::: ) ))))) ; 
 scheme  :: ZF_LANG1:sch 1 ZFInduction{ P1[  ($#m2_finseq_1 :::"ZF-formula":::)] } : 
(Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) "holds"  (Bool P1[(Set (Var "H"))]))
 provided
(Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"   (Bool  "("  (Bool P1[(Set (Set (Var "x1"))  ($#k4_zf_lang :::"'='"::: )  (Set (Var "x2")))]) & (Bool P1[(Set (Set (Var "x1"))  ($#k5_zf_lang :::"'in'"::: )  (Set (Var "x2")))])  ")" ))
 and  
(Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  "st" (Bool (Bool P1[(Set (Var "H"))])) "holds"  (Bool P1[(Set   ($#k6_zf_lang :::"'not'"::: )  (Set (Var "H")))]))
 and  
(Bool  "for" (Set (Var "H1")) "," (Set (Var "H2")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  "st" (Bool (Bool P1[(Set (Var "H1"))]) & (Bool P1[(Set (Var "H2"))])) "holds"  (Bool P1[(Set (Set (Var "H1"))  ($#k7_zf_lang :::"'&'"::: )  (Set (Var "H2")))]))
 and  
(Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m2_subset_1 :::"Variable":::)  "st" (Bool (Bool P1[(Set (Var "H"))])) "holds"  (Bool P1[(Set   ($#k8_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "H")) ")" )])))
 proof 


end; 










definitionlet "D", "D1", "D2" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "D")) "," (Set (Const "D1")); assume 
(Bool (Set (Const "D1"))  ($#r1_tarski :::"c="::: )  (Set (Const "D2")))
 ; func "D2" :::"!"::: "f" ->   ($#m1_subset_1 :::"Function":::) "of" "D" "," "D2" equals :: ZF_LANG1:def 1 "f"; end; 









:: deftheorem    defines :::"!"::: ZF_LANG1:def 1 :  (Bool  "for" (Set (Var "D")) "," (Set (Var "D1")) "," (Set (Var "D2")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set (Var "D1"))  "st" (Bool (Bool (Set (Var "D1"))  ($#r1_tarski :::"c="::: )  (Set (Var "D2")))) "holds"  (Bool (Set (Set (Var "D2"))  ($#k1_zf_lang1 :::"!"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "f"))))); 
 notationlet "E" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Const "E")); let "x" be   ($#m2_subset_1 :::"Variable":::); let "e" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "E")); synonym "f" :::"/":::  "(" "x" "," "e" ")"  for "E" :::"+*":::  "(" "f" "," "x" ")" ; end; definitionlet "E" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Const "E")); let "x" be   ($#m2_subset_1 :::"Variable":::); let "e" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "E")); :: original: :::"/"::: redefine func "f" :::"/":::  "(" "x" "," "e" ")"  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," "E"; end; 
theorem :: ZF_LANG1:71 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (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 "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set   ($#k8_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "H")) ")" )) "iff" (Bool  "for" (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "M")) "holds"  (Bool (Set (Var "M")) "," (Set (Set (Var "v"))  ($#k2_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "m")) ")" )  ($#r1_zf_model :::"|="::: )  (Set (Var "H"))))  ")" ))))) ; 
 
theorem :: ZF_LANG1:72 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (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 "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set   ($#k8_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (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   ($#k8_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "H")) ")" ))  ")" )))))) ; 
 
theorem :: ZF_LANG1:73 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (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 "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set   ($#k13_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "H")) ")" )) "iff" (Bool  "ex" (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "M")) "st" (Bool (Set (Var "M")) "," (Set (Set (Var "v"))  ($#k2_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "m")) ")" )  ($#r1_zf_model :::"|="::: )  (Set (Var "H"))))  ")" ))))) ; 
 
theorem :: ZF_LANG1:74 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (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 "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set   ($#k13_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (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   ($#k13_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "H")) ")" ))  ")" )))))) ; 
 
theorem :: ZF_LANG1:75 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "," (Set (Var "v9")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M"))  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"   ($#m2_subset_1 :::"Variable":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_zf_model :::"Free"::: )  (Set (Var "H"))))) "holds"  (Bool (Set (Set (Var "v9"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "v"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x"))))  ")" ) & (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Var "H")))) "holds"  (Bool (Set (Var "M")) "," (Set (Var "v9"))  ($#r1_zf_model :::"|="::: )  (Set (Var "H")))))) ; 
 registrationlet "H" be   ($#m2_finseq_1 :::"ZF-formula":::); 
cluster (Set   ($#k1_zf_model :::"Free"::: )  "H") ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; 




theorem :: ZF_LANG1:76 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set   ($#k2_zf_lang :::"x."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_zf_lang :::"x."::: )  (Set (Var "j"))))) "holds"  (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set (Var "j")))) ; 
 
theorem :: ZF_LANG1:77 (Bool  "for" (Set (Var "x")) "being"   ($#m2_subset_1 :::"Variable":::) (Bool  "ex" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_zf_lang :::"x."::: )  (Set (Var "i")))))) ; 
 
theorem :: ZF_LANG1:78 (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 "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds"  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Set (Var "x"))  ($#k4_zf_lang :::"'='"::: )  (Set (Var "x"))))))) ; 
 
theorem :: ZF_LANG1:79 (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"::: )   "holds"  (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set (Var "x"))  ($#k4_zf_lang :::"'='"::: )  (Set (Var "x")))))) ; 
 
theorem :: ZF_LANG1:80 (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 "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M"))  "holds" (Bool (Bool  "not" (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Set (Var "x"))  ($#k5_zf_lang :::"'in'"::: )  (Set (Var "x")))))))) ; 
 
theorem :: ZF_LANG1:81 (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"::: )   "holds"   (Bool  "("  (Bool (Bool  "not" (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set (Var "x"))  ($#k5_zf_lang :::"'in'"::: )  (Set (Var "x"))))) & (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set   ($#k6_zf_lang :::"'not'"::: )  (Set  "(" (Set (Var "x"))  ($#k5_zf_lang :::"'in'"::: )  (Set (Var "x")) ")" )))  ")" ))) ; 
 
theorem :: ZF_LANG1:82 (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"::: )   "holds"   (Bool  "("  (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set (Var "x"))  ($#k4_zf_lang :::"'='"::: )  (Set (Var "y")))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y"))) "or" (Bool  "ex" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) )  ($#r1_hidden :::"="::: )  (Set (Var "M"))))  ")" )  ")" ))) ; 
 
theorem :: ZF_LANG1:83 (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"::: )   "holds"   (Bool  "("  (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set   ($#k6_zf_lang :::"'not'"::: )  (Set  "(" (Set (Var "x"))  ($#k5_zf_lang :::"'in'"::: )  (Set (Var "y")) ")" ))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y"))) "or" (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) "holds"  (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "M"))))  ")" )  ")" ))) ; 
 
theorem :: ZF_LANG1:84 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M"))  "st" (Bool (Bool (Set (Var "H")) "is"   ($#v2_zf_lang :::"being_equality"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Var "H"))) "iff" (Bool (Set (Set (Var "v"))  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k18_zf_lang :::"Var1"::: )  (Set (Var "H")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "v"))  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k19_zf_lang :::"Var2"::: )  (Set (Var "H")) ")" )))  ")" )))) ; 
 
theorem :: ZF_LANG1:85 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M"))  "st" (Bool (Bool (Set (Var "H")) "is"   ($#v3_zf_lang :::"being_membership"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Var "H"))) "iff" (Bool (Set (Set (Var "v"))  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k18_zf_lang :::"Var1"::: )  (Set (Var "H")) ")" ))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "v"))  ($#k3_funct_2 :::"."::: )  (Set  "("  ($#k19_zf_lang :::"Var2"::: )  (Set (Var "H")) ")" )))  ")" )))) ; 
 
theorem :: ZF_LANG1:86 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M"))  "st" (Bool (Bool (Set (Var "H")) "is"   ($#v4_zf_lang :::"negative"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Var "H"))) "iff" (Bool (Bool  "not" (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set   ($#k20_zf_lang :::"the_argument_of"::: )  (Set (Var "H")))))  ")" )))) ; 
 
theorem :: ZF_LANG1:87 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M"))  "st" (Bool (Bool (Set (Var "H")) "is"   ($#v5_zf_lang :::"conjunctive"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Var "H"))) "iff" (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set   ($#k21_zf_lang :::"the_left_argument_of"::: )  (Set (Var "H")))) & (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set   ($#k22_zf_lang :::"the_right_argument_of"::: )  (Set (Var "H"))))  ")" )  ")" )))) ; 
 
theorem :: ZF_LANG1:88 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M"))  "st" (Bool (Bool (Set (Var "H")) "is"   ($#v6_zf_lang :::"universal"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Var "H"))) "iff" (Bool  "for" (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "M")) "holds"  (Bool (Set (Var "M")) "," (Set (Set (Var "v"))  ($#k2_zf_lang1 :::"/"::: )   "(" (Set  "("  ($#k23_zf_lang :::"bound_in"::: )  (Set (Var "H")) ")" ) "," (Set (Var "m")) ")" )  ($#r1_zf_model :::"|="::: )  (Set   ($#k24_zf_lang :::"the_scope_of"::: )  (Set (Var "H")))))  ")" )))) ; 
 
theorem :: ZF_LANG1:89 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M"))  "st" (Bool (Bool (Set (Var "H")) "is"   ($#v8_zf_lang :::"disjunctive"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Var "H"))) "iff" (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set   ($#k21_zf_lang :::"the_left_argument_of"::: )  (Set (Var "H")))) "or" (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set   ($#k22_zf_lang :::"the_right_argument_of"::: )  (Set (Var "H"))))  ")" )  ")" )))) ; 
 
theorem :: ZF_LANG1:90 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M"))  "st" (Bool (Bool (Set (Var "H")) "is"   ($#v9_zf_lang :::"conditional"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Var "H"))) "iff"  "("  (Bool (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set   ($#k25_zf_lang :::"the_antecedent_of"::: )  (Set (Var "H"))))) "implies" (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set   ($#k26_zf_lang :::"the_consequent_of"::: )  (Set (Var "H"))))  ")"   ")" )))) ; 
 
theorem :: ZF_LANG1:91 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M"))  "st" (Bool (Bool (Set (Var "H")) "is"   ($#v10_zf_lang :::"biconditional"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Var "H"))) "iff" (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set   ($#k27_zf_lang :::"the_left_side_of"::: )  (Set (Var "H")))) "iff" (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set   ($#k28_zf_lang :::"the_right_side_of"::: )  (Set (Var "H"))))  ")" )  ")" )))) ; 
 
theorem :: ZF_LANG1:92 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M"))  "st" (Bool (Bool (Set (Var "H")) "is"   ($#v11_zf_lang :::"existential"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Var "H"))) "iff" (Bool  "ex" (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "M")) "st" (Bool (Set (Var "M")) "," (Set (Set (Var "v"))  ($#k2_zf_lang1 :::"/"::: )   "(" (Set  "("  ($#k23_zf_lang :::"bound_in"::: )  (Set (Var "H")) ")" ) "," (Set (Var "m")) ")" )  ($#r1_zf_model :::"|="::: )  (Set   ($#k24_zf_lang :::"the_scope_of"::: )  (Set (Var "H")))))  ")" )))) ; 
 
theorem :: ZF_LANG1:93 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (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"::: )   "holds"   (Bool  "("  (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set   ($#k13_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "H")) ")" )) "iff" (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) (Bool  "ex" (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "M")) "st" (Bool (Set (Var "M")) "," (Set (Set (Var "v"))  ($#k2_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "m")) ")" )  ($#r1_zf_model :::"|="::: )  (Set (Var "H")))))  ")" )))) ; 
 
theorem :: ZF_LANG1:94 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (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"::: )    "st" (Bool (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Var "H")))) "holds"  (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set   ($#k13_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "H")) ")" ))))) ; 
 
theorem :: ZF_LANG1:95 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (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"::: )   "holds"   (Bool  "("  (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Var "H"))) "iff" (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set   ($#k14_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "H")) ")" ))  ")" )))) ; 
 
theorem :: ZF_LANG1:96 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (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"::: )    "st" (Bool (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Var "H")))) "holds"  (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set   ($#k15_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "H")) ")" ))))) ; 
 
theorem :: ZF_LANG1:97 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (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"::: )   "holds"   (Bool  "("  (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Var "H"))) "iff" (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set   ($#k16_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "H")) ")" ))  ")" )))) ; 
 
theorem :: ZF_LANG1:98 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (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"::: )    "st" (Bool (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Var "H")))) "holds"  (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set   ($#k17_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "H")) ")" ))))) ; 
 
theorem :: ZF_LANG1:99 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k12_zf_lang :::"<=>"::: )  (Set (Var "q")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "q")) ")" ))) & (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k12_zf_lang :::"<=>"::: )  (Set (Var "q")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "q")) ")" )))  ")" )))) ; 
 
theorem :: ZF_LANG1:100 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k12_zf_lang :::"<=>"::: )  (Set (Var "q")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "p")) ")" ))) & (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k12_zf_lang :::"<=>"::: )  (Set (Var "q")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "p")) ")" )))  ")" )))) ; 
 
theorem :: ZF_LANG1:101 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "q")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "r")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "r")) ")" ) ")" ))))) ; 
 
theorem :: ZF_LANG1:102 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M"))  "st" (Bool (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "q")))) & (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Set (Var "q"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "r"))))) "holds"  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "r"))))))) ; 
 
theorem :: ZF_LANG1:103 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "q")))) & (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set (Var "q"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "r"))))) "holds"  (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "r")))))) ; 
 
theorem :: ZF_LANG1:104 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Set  "(" (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "q")) ")" )  ($#k7_zf_lang :::"'&'"::: )  (Set  "(" (Set (Var "q"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "r")) ")" ) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "r")) ")" ))) & (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set  "(" (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "q")) ")" )  ($#k7_zf_lang :::"'&'"::: )  (Set  "(" (Set (Var "q"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "r")) ")" ) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "r")) ")" )))  ")" )))) ; 
 
theorem :: ZF_LANG1:105 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "p")) ")" ))) & (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "p")) ")" )))  ")" )))) ; 
 
theorem :: ZF_LANG1:106 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "r")) ")" ) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "q")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "r")) ")" ) ")" ))) & (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "r")) ")" ) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "q")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "r")) ")" ) ")" )))  ")" )))) ; 
 
theorem :: ZF_LANG1:107 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k7_zf_lang :::"'&'"::: )  (Set (Var "q")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set (Var "p")))) & (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k7_zf_lang :::"'&'"::: )  (Set (Var "q")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set (Var "p"))))  ")" )))) ; 
 
theorem :: ZF_LANG1:108 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k7_zf_lang :::"'&'"::: )  (Set (Var "q")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set (Var "q")))) & (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k7_zf_lang :::"'&'"::: )  (Set (Var "q")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set (Var "q"))))  ")" )))) ; 
 
theorem :: ZF_LANG1:109 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k7_zf_lang :::"'&'"::: )  (Set (Var "q")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k7_zf_lang :::"'&'"::: )  (Set (Var "p")) ")" ))) & (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k7_zf_lang :::"'&'"::: )  (Set (Var "q")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k7_zf_lang :::"'&'"::: )  (Set (Var "p")) ")" )))  ")" )))) ; 
 
theorem :: ZF_LANG1:110 (Bool  "for" (Set (Var "p")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k7_zf_lang :::"'&'"::: )  (Set (Var "p")) ")" ))) & (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k7_zf_lang :::"'&'"::: )  (Set (Var "p")) ")" )))  ")" )))) ; 
 
theorem :: ZF_LANG1:111 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "q")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "r")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k7_zf_lang :::"'&'"::: )  (Set (Var "r")) ")" ) ")" ) ")" ))) & (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "q")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "r")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k7_zf_lang :::"'&'"::: )  (Set (Var "r")) ")" ) ")" ) ")" )))  ")" )))) ; 
 
theorem :: ZF_LANG1:112 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "q")) ")" ))) & (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "q")) ")" )))  ")" )))) ; 
 
theorem :: ZF_LANG1:113 (Bool  "for" (Set (Var "q")) "," (Set (Var "p")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Set (Var "q"))  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "q")) ")" ))) & (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set (Var "q"))  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "q")) ")" )))  ")" )))) ; 
 
theorem :: ZF_LANG1:114 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "q")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "p")) ")" ))) & (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "q")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "p")) ")" )))  ")" )))) ; 
 
theorem :: ZF_LANG1:115 (Bool  "for" (Set (Var "p")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "p")) ")" ))) & (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "p")) ")" )))  ")" )))) ; 
 
theorem :: ZF_LANG1:116 (Bool  "for" (Set (Var "p")) "," (Set (Var "r")) "," (Set (Var "q")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "r")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "r")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "q")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set (Var "r")) ")" ) ")" ))) & (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "r")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "r")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "q")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set (Var "r")) ")" ) ")" )))  ")" )))) ; 
 
theorem :: ZF_LANG1:117 (Bool  "for" (Set (Var "p")) "," (Set (Var "r")) "," (Set (Var "q")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Set  "(" (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "r")) ")" )  ($#k7_zf_lang :::"'&'"::: )  (Set  "(" (Set (Var "q"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "r")) ")" ) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "q")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set (Var "r")) ")" ))) & (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set  "(" (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "r")) ")" )  ($#k7_zf_lang :::"'&'"::: )  (Set  "(" (Set (Var "q"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "r")) ")" ) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "q")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set (Var "r")) ")" )))  ")" )))) ; 
 
theorem :: ZF_LANG1:118 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "q")) ")" ) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k11_zf_lang :::"=>"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "p")) ")" ) ")" ))) & (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "q")) ")" ) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k11_zf_lang :::"=>"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "p")) ")" ) ")" )))  ")" )))) ; 
 
theorem :: ZF_LANG1:119 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "q")) ")" ))) & (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "q")) ")" )))  ")" )))) ; 
 
theorem :: ZF_LANG1:120 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Set  "(" (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "q")) ")" )  ($#k7_zf_lang :::"'&'"::: )  (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "q")) ")" ) ")" ) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "p")) ")" ))) & (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set  "(" (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "q")) ")" )  ($#k7_zf_lang :::"'&'"::: )  (Set  "(" (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "q")) ")" ) ")" ) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "p")) ")" )))  ")" )))) ; 
 
theorem :: ZF_LANG1:121 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set (Var "p"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "q")))) & (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Var "p")))) "holds"  (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Var "q"))))) ; 
 
theorem :: ZF_LANG1:122 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set  "(" (Set (Var "p"))  ($#k7_zf_lang :::"'&'"::: )  (Set (Var "q")) ")" ) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k10_zf_lang :::"'or'"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "q")) ")" ) ")" ))) & (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set  "(" (Set (Var "p"))  ($#k7_zf_lang :::"'&'"::: )  (Set (Var "q")) ")" ) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k10_zf_lang :::"'or'"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "q")) ")" ) ")" )))  ")" )))) ; 
 
theorem :: ZF_LANG1:123 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Set  "(" (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k10_zf_lang :::"'or'"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "q")) ")" ) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set  "(" (Set (Var "p"))  ($#k7_zf_lang :::"'&'"::: )  (Set (Var "q")) ")" ) ")" ))) & (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set  "(" (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k10_zf_lang :::"'or'"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "q")) ")" ) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set  "(" (Set (Var "p"))  ($#k7_zf_lang :::"'&'"::: )  (Set (Var "q")) ")" ) ")" )))  ")" )))) ; 
 
theorem :: ZF_LANG1:124 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set  "(" (Set (Var "p"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "q")) ")" ) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k7_zf_lang :::"'&'"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "q")) ")" ) ")" ))) & (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set  "(" (Set (Var "p"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "q")) ")" ) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k7_zf_lang :::"'&'"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "q")) ")" ) ")" )))  ")" )))) ; 
 
theorem :: ZF_LANG1:125 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "M")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "M")) "," (Set (Var "v"))  ($#r1_zf_model :::"|="::: )  (Set (Set  "(" (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k7_zf_lang :::"'&'"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "q")) ")" ) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set  "(" (Set (Var "p"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "q")) ")" ) ")" ))) & (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set  "(" (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k7_zf_lang :::"'&'"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "q")) ")" ) ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set  "(" (Set (Var "p"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "q")) ")" ) ")" )))  ")" )))) ; 
 
theorem :: ZF_LANG1:126 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (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"::: )   "holds"  (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set  "("  ($#k8_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "H")) ")"  ")" )  ($#k11_zf_lang :::"=>"::: )  (Set (Var "H"))))))) ; 
 
theorem :: ZF_LANG1:127 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (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"::: )   "holds"  (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set (Var "H"))  ($#k11_zf_lang :::"=>"::: )  (Set  "("  ($#k13_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "H")) ")"  ")" )))))) ; 
 
theorem :: ZF_LANG1:128 (Bool  "for" (Set (Var "H1")) "," (Set (Var "H2")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (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"::: )    "st" (Bool (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_zf_model :::"Free"::: )  (Set (Var "H1")))))) "holds"  (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set  "("  ($#k8_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set  "(" (Set (Var "H1"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "H2")) ")" ) ")"  ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set (Var "H1"))  ($#k11_zf_lang :::"=>"::: )  (Set  "("  ($#k8_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "H2")) ")"  ")" ) ")" )))))) ; 
 
theorem :: ZF_LANG1:129 (Bool  "for" (Set (Var "H1")) "," (Set (Var "H2")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (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"::: )    "st" (Bool (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_zf_model :::"Free"::: )  (Set (Var "H1"))))) & (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set (Var "H1"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "H2"))))) "holds"  (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set (Var "H1"))  ($#k11_zf_lang :::"=>"::: )  (Set  "("  ($#k8_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "H2")) ")"  ")" )))))) ; 
 
theorem :: ZF_LANG1:130 (Bool  "for" (Set (Var "H2")) "," (Set (Var "H1")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (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"::: )    "st" (Bool (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_zf_model :::"Free"::: )  (Set (Var "H2")))))) "holds"  (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set  "("  ($#k8_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set  "(" (Set (Var "H1"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "H2")) ")" ) ")"  ")" )  ($#k11_zf_lang :::"=>"::: )  (Set  "(" (Set  "("  ($#k13_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "H1")) ")"  ")" )  ($#k11_zf_lang :::"=>"::: )  (Set (Var "H2")) ")" )))))) ; 
 
theorem :: ZF_LANG1:131 (Bool  "for" (Set (Var "H2")) "," (Set (Var "H1")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (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"::: )    "st" (Bool (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_zf_model :::"Free"::: )  (Set (Var "H2"))))) & (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set (Var "H1"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "H2"))))) "holds"  (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set  "("  ($#k13_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "H1")) ")"  ")" )  ($#k11_zf_lang :::"=>"::: )  (Set (Var "H2"))))))) ; 
 
theorem :: ZF_LANG1:132 (Bool  "for" (Set (Var "H1")) "," (Set (Var "H2")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (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"::: )    "st" (Bool (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set (Var "H1"))  ($#k11_zf_lang :::"=>"::: )  (Set  "("  ($#k8_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "H2")) ")"  ")" )))) "holds"  (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set (Var "H1"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "H2"))))))) ; 
 
theorem :: ZF_LANG1:133 (Bool  "for" (Set (Var "H1")) "," (Set (Var "H2")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (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"::: )    "st" (Bool (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set  "("  ($#k13_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "H1")) ")"  ")" )  ($#k11_zf_lang :::"=>"::: )  (Set (Var "H2"))))) "holds"  (Bool (Set (Var "M"))  ($#r2_zf_model :::"|="::: )  (Set (Set (Var "H1"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "H2"))))))) ; 
 
theorem :: ZF_LANG1:134 (Bool (Set   ($#k9_zf_lang :::"WFF"::: )  )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) ; 
 definitionlet "H" be   ($#m2_finseq_1 :::"ZF-formula":::); func  :::"variables_in"::: "H" ->    ($#m1_hidden :::"set"::: )   equals :: ZF_LANG1:def 2 (Set (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  "H" ")" )  ($#k6_subset_1 :::"\"::: )  (Set  ($#k3_enumset1 :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) "," (Num 3) "," (Num 4) ($#k3_enumset1 :::"}"::: ) )); end; 





:: deftheorem    defines :::"variables_in"::: ZF_LANG1:def 2 :  (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) "holds"  (Bool (Set   ($#k3_zf_lang1 :::"variables_in"::: )  (Set (Var "H")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "H")) ")" )  ($#k6_subset_1 :::"\"::: )  (Set  ($#k3_enumset1 :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) "," (Num 3) "," (Num 4) ($#k3_enumset1 :::"}"::: ) )))); 
 
theorem :: ZF_LANG1:135 (Bool  "for" (Set (Var "x")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Num 1)) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Num 2)) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Num 3)) & (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Num 4))  ")" )) ; 
 
theorem :: ZF_LANG1:136 (Bool  "for" (Set (Var "x")) "being"   ($#m2_subset_1 :::"Variable":::)  "holds" (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k3_enumset1 :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) "," (Num 3) "," (Num 4) ($#k3_enumset1 :::"}"::: ) )))) ; 
 
theorem :: ZF_LANG1:137 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_zf_lang1 :::"variables_in"::: )  (Set (Var "H"))))) "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Num 1)) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Num 2)) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Num 3)) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Num 4))  ")" ))) ; 
 
theorem :: ZF_LANG1:138 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"  (Bool (Set   ($#k3_zf_lang1 :::"variables_in"::: )  (Set  "(" (Set (Var "x"))  ($#k4_zf_lang :::"'='"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ))) ; 
 
theorem :: ZF_LANG1:139 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"  (Bool (Set   ($#k3_zf_lang1 :::"variables_in"::: )  (Set  "(" (Set (Var "x"))  ($#k5_zf_lang :::"'in'"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ))) ; 
 
theorem :: ZF_LANG1:140 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) "holds"  (Bool (Set   ($#k3_zf_lang1 :::"variables_in"::: )  (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "H")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_zf_lang1 :::"variables_in"::: )  (Set (Var "H"))))) ; 
 
theorem :: ZF_LANG1:141 (Bool  "for" (Set (Var "H1")) "," (Set (Var "H2")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) "holds"  (Bool (Set   ($#k3_zf_lang1 :::"variables_in"::: )  (Set  "(" (Set (Var "H1"))  ($#k7_zf_lang :::"'&'"::: )  (Set (Var "H2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_zf_lang1 :::"variables_in"::: )  (Set (Var "H1")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "("  ($#k3_zf_lang1 :::"variables_in"::: )  (Set (Var "H2")) ")" )))) ; 
 
theorem :: ZF_LANG1:142 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"  (Bool (Set   ($#k3_zf_lang1 :::"variables_in"::: )  (Set  "("  ($#k8_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "H")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_zf_lang1 :::"variables_in"::: )  (Set (Var "H")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))))) ; 
 
theorem :: ZF_LANG1:143 (Bool  "for" (Set (Var "H1")) "," (Set (Var "H2")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) "holds"  (Bool (Set   ($#k3_zf_lang1 :::"variables_in"::: )  (Set  "(" (Set (Var "H1"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "H2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_zf_lang1 :::"variables_in"::: )  (Set (Var "H1")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "("  ($#k3_zf_lang1 :::"variables_in"::: )  (Set (Var "H2")) ")" )))) ; 
 
theorem :: ZF_LANG1:144 (Bool  "for" (Set (Var "H1")) "," (Set (Var "H2")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) "holds"  (Bool (Set   ($#k3_zf_lang1 :::"variables_in"::: )  (Set  "(" (Set (Var "H1"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "H2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_zf_lang1 :::"variables_in"::: )  (Set (Var "H1")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "("  ($#k3_zf_lang1 :::"variables_in"::: )  (Set (Var "H2")) ")" )))) ; 
 
theorem :: ZF_LANG1:145 (Bool  "for" (Set (Var "H1")) "," (Set (Var "H2")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) "holds"  (Bool (Set   ($#k3_zf_lang1 :::"variables_in"::: )  (Set  "(" (Set (Var "H1"))  ($#k12_zf_lang :::"<=>"::: )  (Set (Var "H2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_zf_lang1 :::"variables_in"::: )  (Set (Var "H1")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "("  ($#k3_zf_lang1 :::"variables_in"::: )  (Set (Var "H2")) ")" )))) ; 
 
theorem :: ZF_LANG1:146 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"  (Bool (Set   ($#k3_zf_lang1 :::"variables_in"::: )  (Set  "("  ($#k13_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "H")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_zf_lang1 :::"variables_in"::: )  (Set (Var "H")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))))) ; 
 
theorem :: ZF_LANG1:147 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"  (Bool (Set   ($#k3_zf_lang1 :::"variables_in"::: )  (Set  "("  ($#k14_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "H")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_zf_lang1 :::"variables_in"::: )  (Set (Var "H")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ))))) ; 
 
theorem :: ZF_LANG1:148 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"  (Bool (Set   ($#k3_zf_lang1 :::"variables_in"::: )  (Set  "("  ($#k15_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "H")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_zf_lang1 :::"variables_in"::: )  (Set (Var "H")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ))))) ; 
 
theorem :: ZF_LANG1:149 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"  (Bool (Set   ($#k3_zf_lang1 :::"variables_in"::: )  (Set  "("  ($#k16_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "H")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_zf_lang1 :::"variables_in"::: )  (Set (Var "H")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_enumset1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k1_enumset1 :::"}"::: ) ))))) ; 
 
theorem :: ZF_LANG1:150 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"  (Bool (Set   ($#k3_zf_lang1 :::"variables_in"::: )  (Set  "("  ($#k17_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "H")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_zf_lang1 :::"variables_in"::: )  (Set (Var "H")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_enumset1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k1_enumset1 :::"}"::: ) ))))) ; 
 
theorem :: ZF_LANG1:151 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) "holds"  (Bool (Set   ($#k2_zf_model :::"Free"::: )  (Set (Var "H")))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_zf_lang1 :::"variables_in"::: )  (Set (Var "H"))))) ; 
 definitionlet "H" be   ($#m2_finseq_1 :::"ZF-formula":::); :: original: :::"variables_in"::: redefine func  :::"variables_in"::: "H" ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ); end; definitionlet "H" be   ($#m2_finseq_1 :::"ZF-formula":::); let "x", "y" be   ($#m2_subset_1 :::"Variable":::); func "H" :::"/":::  "(" "x" "," "y" ")"  ->   ($#m1_hidden :::"Function":::) means :: ZF_LANG1:def 3 (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  "H")) & (Bool  "("   "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  "H"))) "holds"  (Bool  "("   "("  (Bool (Bool (Set "H"  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  "x")) "implies" (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  "y")  ")"  &  "("  (Bool (Bool (Set "H"  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"<>"::: )  "x")) "implies" (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set "H"  ($#k1_funct_1 :::"."::: )  (Set (Var "a"))))  ")"   ")" )  ")" )  ")" ); end; 







:: deftheorem    defines :::"/"::: ZF_LANG1:def 3 :  (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::)  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "H"))  ($#k5_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b4")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "H")))) & (Bool  "("   "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "H"))))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Set (Var "H"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "x")))) "implies" (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "y")))  ")"  &  "("  (Bool (Bool (Set (Set (Var "H"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"<>"::: )  (Set (Var "x")))) "implies" (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "H"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a"))))  ")"   ")" )  ")" )  ")" )  ")" )))); 
 
theorem :: ZF_LANG1:152 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set (Var "x1"))  ($#k4_zf_lang :::"'='"::: )  (Set (Var "x2")) ")" )  ($#k5_zf_lang1 :::"/"::: )   "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "z1"))  ($#k4_zf_lang :::"'='"::: )  (Set (Var "z2")))) "iff" (Bool  "("  (Bool  "("  (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y1"))) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y1"))) & (Bool (Set (Var "z1"))  ($#r1_hidden :::"="::: )  (Set (Var "x1"))) & (Bool (Set (Var "z2"))  ($#r1_hidden :::"="::: )  (Set (Var "x2")))  ")" ) "or" (Bool  "("  (Bool (Set (Var "x1"))  ($#r1_hidden :::"="::: )  (Set (Var "y1"))) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y1"))) & (Bool (Set (Var "z1"))  ($#r1_hidden :::"="::: )  (Set (Var "y2"))) & (Bool (Set (Var "z2"))  ($#r1_hidden :::"="::: )  (Set (Var "x2")))  ")" ) "or" (Bool  "("  (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y1"))) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"="::: )  (Set (Var "y1"))) & (Bool (Set (Var "z1"))  ($#r1_hidden :::"="::: )  (Set (Var "x1"))) & (Bool (Set (Var "z2"))  ($#r1_hidden :::"="::: )  (Set (Var "y2")))  ")" ) "or" (Bool  "("  (Bool (Set (Var "x1"))  ($#r1_hidden :::"="::: )  (Set (Var "y1"))) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"="::: )  (Set (Var "y1"))) & (Bool (Set (Var "z1"))  ($#r1_hidden :::"="::: )  (Set (Var "y2"))) & (Bool (Set (Var "z2"))  ($#r1_hidden :::"="::: )  (Set (Var "y2")))  ")" )  ")" )  ")" )) ; 
 
theorem :: ZF_LANG1:153 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being"   ($#m2_subset_1 :::"Variable":::) (Bool  "ex" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#m2_subset_1 :::"Variable":::) "st" (Bool (Set (Set  "(" (Set (Var "x1"))  ($#k4_zf_lang :::"'='"::: )  (Set (Var "x2")) ")" )  ($#k5_zf_lang1 :::"/"::: )   "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "z1"))  ($#k4_zf_lang :::"'='"::: )  (Set (Var "z2")))))) ; 
 
theorem :: ZF_LANG1:154 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set (Var "x1"))  ($#k5_zf_lang :::"'in'"::: )  (Set (Var "x2")) ")" )  ($#k5_zf_lang1 :::"/"::: )   "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "z1"))  ($#k5_zf_lang :::"'in'"::: )  (Set (Var "z2")))) "iff" (Bool  "("  (Bool  "("  (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y1"))) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y1"))) & (Bool (Set (Var "z1"))  ($#r1_hidden :::"="::: )  (Set (Var "x1"))) & (Bool (Set (Var "z2"))  ($#r1_hidden :::"="::: )  (Set (Var "x2")))  ")" ) "or" (Bool  "("  (Bool (Set (Var "x1"))  ($#r1_hidden :::"="::: )  (Set (Var "y1"))) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y1"))) & (Bool (Set (Var "z1"))  ($#r1_hidden :::"="::: )  (Set (Var "y2"))) & (Bool (Set (Var "z2"))  ($#r1_hidden :::"="::: )  (Set (Var "x2")))  ")" ) "or" (Bool  "("  (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y1"))) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"="::: )  (Set (Var "y1"))) & (Bool (Set (Var "z1"))  ($#r1_hidden :::"="::: )  (Set (Var "x1"))) & (Bool (Set (Var "z2"))  ($#r1_hidden :::"="::: )  (Set (Var "y2")))  ")" ) "or" (Bool  "("  (Bool (Set (Var "x1"))  ($#r1_hidden :::"="::: )  (Set (Var "y1"))) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"="::: )  (Set (Var "y1"))) & (Bool (Set (Var "z1"))  ($#r1_hidden :::"="::: )  (Set (Var "y2"))) & (Bool (Set (Var "z2"))  ($#r1_hidden :::"="::: )  (Set (Var "y2")))  ")" )  ")" )  ")" )) ; 
 
theorem :: ZF_LANG1:155 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being"   ($#m2_subset_1 :::"Variable":::) (Bool  "ex" (Set (Var "z1")) "," (Set (Var "z2")) "being"   ($#m2_subset_1 :::"Variable":::) "st" (Bool (Set (Set  "(" (Set (Var "x1"))  ($#k5_zf_lang :::"'in'"::: )  (Set (Var "x2")) ")" )  ($#k5_zf_lang1 :::"/"::: )   "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "z1"))  ($#k5_zf_lang :::"'in'"::: )  (Set (Var "z2")))))) ; 
 
theorem :: ZF_LANG1:156 (Bool  "for" (Set (Var "F")) "," (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"   (Bool  "("  (Bool (Set   ($#k6_zf_lang :::"'not'"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_zf_lang :::"'not'"::: )  (Set (Var "H")) ")" )  ($#k5_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool (Set (Var "F"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "H"))  ($#k5_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))  ")" ))) ; 
 
theorem :: ZF_LANG1:157 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"  (Bool (Set (Set (Var "H"))  ($#k5_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r2_hidden :::"in"::: )  (Set   ($#k9_zf_lang :::"WFF"::: )  )))) ; 
 definitionlet "H" be   ($#m2_finseq_1 :::"ZF-formula":::); let "x", "y" be   ($#m2_subset_1 :::"Variable":::); :: original: :::"/"::: redefine func "H" :::"/":::  "(" "x" "," "y" ")"  ->   ($#m2_finseq_1 :::"ZF-formula":::); end; 
theorem :: ZF_LANG1:158 (Bool  "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "H1")) "," (Set (Var "H2")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"   (Bool  "("  (Bool (Set (Set (Var "G1"))  ($#k7_zf_lang :::"'&'"::: )  (Set (Var "G2")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "H1"))  ($#k7_zf_lang :::"'&'"::: )  (Set (Var "H2")) ")" )  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "G1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "H1"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) & (Bool (Set (Var "G2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "H2"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))  ")" )  ")" ))) ; 
 
theorem :: ZF_LANG1:159 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "z")) "," (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::)  "st" (Bool (Bool (Set (Var "z"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x")))) "holds"  (Bool  "("  (Bool (Set   ($#k8_zf_lang :::"All"::: )   "(" (Set (Var "z")) "," (Set (Var "G")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k8_zf_lang :::"All"::: )   "(" (Set (Var "z")) "," (Set (Var "H")) ")"  ")" )  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool (Set (Var "G"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))  ")" ))) ; 
 
theorem :: ZF_LANG1:160 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "y")) "," (Set (Var "x")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"   (Bool  "("  (Bool (Set   ($#k8_zf_lang :::"All"::: )   "(" (Set (Var "y")) "," (Set (Var "G")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k8_zf_lang :::"All"::: )   "(" (Set (Var "x")) "," (Set (Var "H")) ")"  ")" )  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool (Set (Var "G"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))  ")" ))) ; 
 
theorem :: ZF_LANG1:161 (Bool  "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "H1")) "," (Set (Var "H2")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"   (Bool  "("  (Bool (Set (Set (Var "G1"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "G2")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "H1"))  ($#k10_zf_lang :::"'or'"::: )  (Set (Var "H2")) ")" )  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "G1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "H1"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) & (Bool (Set (Var "G2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "H2"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))  ")" )  ")" ))) ; 
 
theorem :: ZF_LANG1:162 (Bool  "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "H1")) "," (Set (Var "H2")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"   (Bool  "("  (Bool (Set (Set (Var "G1"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "G2")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "H1"))  ($#k11_zf_lang :::"=>"::: )  (Set (Var "H2")) ")" )  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "G1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "H1"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) & (Bool (Set (Var "G2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "H2"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))  ")" )  ")" ))) ; 
 
theorem :: ZF_LANG1:163 (Bool  "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "H1")) "," (Set (Var "H2")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"   (Bool  "("  (Bool (Set (Set (Var "G1"))  ($#k12_zf_lang :::"<=>"::: )  (Set (Var "G2")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "H1"))  ($#k12_zf_lang :::"<=>"::: )  (Set (Var "H2")) ")" )  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool  "("  (Bool (Set (Var "G1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "H1"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) & (Bool (Set (Var "G2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "H2"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))  ")" )  ")" ))) ; 
 
theorem :: ZF_LANG1:164 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "z")) "," (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::)  "st" (Bool (Bool (Set (Var "z"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x")))) "holds"  (Bool  "("  (Bool (Set   ($#k13_zf_lang :::"Ex"::: )   "(" (Set (Var "z")) "," (Set (Var "G")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k13_zf_lang :::"Ex"::: )   "(" (Set (Var "z")) "," (Set (Var "H")) ")"  ")" )  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool (Set (Var "G"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))  ")" ))) ; 
 
theorem :: ZF_LANG1:165 (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "y")) "," (Set (Var "x")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"   (Bool  "("  (Bool (Set   ($#k13_zf_lang :::"Ex"::: )   "(" (Set (Var "y")) "," (Set (Var "G")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k13_zf_lang :::"Ex"::: )   "(" (Set (Var "x")) "," (Set (Var "H")) ")"  ")" )  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) "iff" (Bool (Set (Var "G"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))  ")" ))) ; 
 
theorem :: ZF_LANG1:166 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"   (Bool  "("  (Bool (Set (Var "H")) "is"   ($#v2_zf_lang :::"being_equality"::: )  ) "iff" (Bool (Set (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) "is"   ($#v2_zf_lang :::"being_equality"::: )  )  ")" ))) ; 
 
theorem :: ZF_LANG1:167 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"   (Bool  "("  (Bool (Set (Var "H")) "is"   ($#v3_zf_lang :::"being_membership"::: )  ) "iff" (Bool (Set (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) "is"   ($#v3_zf_lang :::"being_membership"::: )  )  ")" ))) ; 
 
theorem :: ZF_LANG1:168 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"   (Bool  "("  (Bool (Set (Var "H")) "is"   ($#v4_zf_lang :::"negative"::: )  ) "iff" (Bool (Set (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) "is"   ($#v4_zf_lang :::"negative"::: )  )  ")" ))) ; 
 
theorem :: ZF_LANG1:169 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"   (Bool  "("  (Bool (Set (Var "H")) "is"   ($#v5_zf_lang :::"conjunctive"::: )  ) "iff" (Bool (Set (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) "is"   ($#v5_zf_lang :::"conjunctive"::: )  )  ")" ))) ; 
 
theorem :: ZF_LANG1:170 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"   (Bool  "("  (Bool (Set (Var "H")) "is"   ($#v6_zf_lang :::"universal"::: )  ) "iff" (Bool (Set (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) "is"   ($#v6_zf_lang :::"universal"::: )  )  ")" ))) ; 
 
theorem :: ZF_LANG1:171 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::)  "st" (Bool (Bool (Set (Var "H")) "is"   ($#v4_zf_lang :::"negative"::: )  )) "holds"  (Bool (Set   ($#k20_zf_lang :::"the_argument_of"::: )  (Set  "(" (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k20_zf_lang :::"the_argument_of"::: )  (Set (Var "H")) ")" )  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))) ; 
 
theorem :: ZF_LANG1:172 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::)  "st" (Bool (Bool (Set (Var "H")) "is"   ($#v5_zf_lang :::"conjunctive"::: )  )) "holds"  (Bool  "("  (Bool (Set   ($#k21_zf_lang :::"the_left_argument_of"::: )  (Set  "(" (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k21_zf_lang :::"the_left_argument_of"::: )  (Set (Var "H")) ")" )  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) & (Bool (Set   ($#k22_zf_lang :::"the_right_argument_of"::: )  (Set  "(" (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k22_zf_lang :::"the_right_argument_of"::: )  (Set (Var "H")) ")" )  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))  ")" ))) ; 
 
theorem :: ZF_LANG1:173 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::)  "st" (Bool (Bool (Set (Var "H")) "is"   ($#v6_zf_lang :::"universal"::: )  )) "holds"  (Bool  "("  (Bool (Set   ($#k24_zf_lang :::"the_scope_of"::: )  (Set  "(" (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k24_zf_lang :::"the_scope_of"::: )  (Set (Var "H")) ")" )  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) &  "("  (Bool (Bool (Set   ($#k23_zf_lang :::"bound_in"::: )  (Set (Var "H")))  ($#r1_hidden :::"="::: )  (Set (Var "x")))) "implies" (Bool (Set   ($#k23_zf_lang :::"bound_in"::: )  (Set  "(" (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "y")))  ")"  &  "("  (Bool (Bool (Set   ($#k23_zf_lang :::"bound_in"::: )  (Set (Var "H")))  ($#r1_hidden :::"<>"::: )  (Set (Var "x")))) "implies" (Bool (Set   ($#k23_zf_lang :::"bound_in"::: )  (Set  "(" (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k23_zf_lang :::"bound_in"::: )  (Set (Var "H"))))  ")"   ")" ))) ; 
 
theorem :: ZF_LANG1:174 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"   (Bool  "("  (Bool (Set (Var "H")) "is"   ($#v8_zf_lang :::"disjunctive"::: )  ) "iff" (Bool (Set (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) "is"   ($#v8_zf_lang :::"disjunctive"::: )  )  ")" ))) ; 
 
theorem :: ZF_LANG1:175 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"   (Bool  "("  (Bool (Set (Var "H")) "is"   ($#v9_zf_lang :::"conditional"::: )  ) "iff" (Bool (Set (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) "is"   ($#v9_zf_lang :::"conditional"::: )  )  ")" ))) ; 
 
theorem :: ZF_LANG1:176 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::)  "st" (Bool (Bool (Set (Var "H")) "is"   ($#v10_zf_lang :::"biconditional"::: )  )) "holds"  (Bool (Set (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) "is"   ($#v10_zf_lang :::"biconditional"::: )  ))) ; 
 
theorem :: ZF_LANG1:177 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"   (Bool  "("  (Bool (Set (Var "H")) "is"   ($#v11_zf_lang :::"existential"::: )  ) "iff" (Bool (Set (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) "is"   ($#v11_zf_lang :::"existential"::: )  )  ")" ))) ; 
 
theorem :: ZF_LANG1:178 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::)  "st" (Bool (Bool (Set (Var "H")) "is"   ($#v8_zf_lang :::"disjunctive"::: )  )) "holds"  (Bool  "("  (Bool (Set   ($#k21_zf_lang :::"the_left_argument_of"::: )  (Set  "(" (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k21_zf_lang :::"the_left_argument_of"::: )  (Set (Var "H")) ")" )  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) & (Bool (Set   ($#k22_zf_lang :::"the_right_argument_of"::: )  (Set  "(" (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k22_zf_lang :::"the_right_argument_of"::: )  (Set (Var "H")) ")" )  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))  ")" ))) ; 
 
theorem :: ZF_LANG1:179 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::)  "st" (Bool (Bool (Set (Var "H")) "is"   ($#v9_zf_lang :::"conditional"::: )  )) "holds"  (Bool  "("  (Bool (Set   ($#k25_zf_lang :::"the_antecedent_of"::: )  (Set  "(" (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k25_zf_lang :::"the_antecedent_of"::: )  (Set (Var "H")) ")" )  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) & (Bool (Set   ($#k26_zf_lang :::"the_consequent_of"::: )  (Set  "(" (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k26_zf_lang :::"the_consequent_of"::: )  (Set (Var "H")) ")" )  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))  ")" ))) ; 
 
theorem :: ZF_LANG1:180 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::)  "st" (Bool (Bool (Set (Var "H")) "is"   ($#v10_zf_lang :::"biconditional"::: )  )) "holds"  (Bool  "("  (Bool (Set   ($#k27_zf_lang :::"the_left_side_of"::: )  (Set  "(" (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k27_zf_lang :::"the_left_side_of"::: )  (Set (Var "H")) ")" )  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) & (Bool (Set   ($#k28_zf_lang :::"the_right_side_of"::: )  (Set  "(" (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k28_zf_lang :::"the_right_side_of"::: )  (Set (Var "H")) ")" )  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))  ")" ))) ; 
 
theorem :: ZF_LANG1:181 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::)  "st" (Bool (Bool (Set (Var "H")) "is"   ($#v11_zf_lang :::"existential"::: )  )) "holds"  (Bool  "("  (Bool (Set   ($#k24_zf_lang :::"the_scope_of"::: )  (Set  "(" (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k24_zf_lang :::"the_scope_of"::: )  (Set (Var "H")) ")" )  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) &  "("  (Bool (Bool (Set   ($#k23_zf_lang :::"bound_in"::: )  (Set (Var "H")))  ($#r1_hidden :::"="::: )  (Set (Var "x")))) "implies" (Bool (Set   ($#k23_zf_lang :::"bound_in"::: )  (Set  "(" (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "y")))  ")"  &  "("  (Bool (Bool (Set   ($#k23_zf_lang :::"bound_in"::: )  (Set (Var "H")))  ($#r1_hidden :::"<>"::: )  (Set (Var "x")))) "implies" (Bool (Set   ($#k23_zf_lang :::"bound_in"::: )  (Set  "(" (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k23_zf_lang :::"bound_in"::: )  (Set (Var "H"))))  ")"   ")" ))) ; 
 
theorem :: ZF_LANG1:182 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::)  "st" (Bool (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_zf_lang1 :::"variables_in"::: )  (Set (Var "H")))))) "holds"  (Bool (Set (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "H"))))) ; 
 
theorem :: ZF_LANG1:183 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"  (Bool (Set (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "H"))))) ; 
 
theorem :: ZF_LANG1:184 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y")))) "holds"  (Bool  "not" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_zf_lang1 :::"variables_in"::: )  (Set  "(" (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" )))))) ; 
 
theorem :: ZF_LANG1:185 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_zf_lang1 :::"variables_in"::: )  (Set (Var "H"))))) "holds"  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_zf_lang1 :::"variables_in"::: )  (Set  "(" (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" ))))) ; 
 
theorem :: ZF_LANG1:186 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"   ($#m2_subset_1 :::"Variable":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y")))) "holds"  (Bool (Set (Set  "(" (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" )  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "z")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))) ; 
 
theorem :: ZF_LANG1:187 (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_subset_1 :::"Variable":::) "holds"  (Bool (Set   ($#k4_zf_lang1 :::"variables_in"::: )  (Set  "(" (Set (Var "H"))  ($#k6_zf_lang1 :::"/"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" ))  ($#r1_tarski :::"c="::: )  (Set (Set  "(" (Set  "("  ($#k4_zf_lang1 :::"variables_in"::: )  (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 :::"}"::: ) ))))) ;