:: WELLSET1  semantic presentation begin  






































theorem :: WELLSET1:1 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R")))) "iff" (Bool  "ex" (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R"))) "or" (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "R")))  ")" ))  ")" ))) ; 
 
theorem :: WELLSET1:2 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "Y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "W"))  ($#r1_hidden :::"="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds"  (Bool (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "W")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")))))) ; 
 scheme  :: WELLSET1:sch 1 RSeparation{ F1() ->    ($#m1_hidden :::"set"::: )  , P1[  ($#m1_hidden :::"Relation":::)] } : 
(Bool  "ex" (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Set (Var "R"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) "iff" (Bool  "("  (Bool (Set (Var "R"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" )) & (Bool P1[(Set (Var "R"))])  ")" )  ")" )))
 proof 


end; 
theorem :: WELLSET1:3 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "W")))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "W")))) & (Bool (Set (Var "W")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  ) & (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "W"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "y")))))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "W"))))) ; 
 
theorem :: WELLSET1:4 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "W")))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "W")))) & (Bool (Set (Var "W")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  ) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "W"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "y"))))) "holds"  (Bool  "not" (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "W")))))) ; 
 
theorem :: WELLSET1:5 (Bool  "for" (Set (Var "F")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "D")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "D")))) "holds"  (Bool  "("  (Bool (Bool  "not" (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) & (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "D"))))  ")" )  ")" )) "holds"  (Bool  "ex" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "st"  (Bool  "("  (Bool (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R")))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "D")))) & (Bool (Set (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  ) & (Bool (Bool  "not" (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R")))  ($#r2_hidden :::"in"::: )  (Set (Var "D")))) & (Bool  "("   "for" (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R"))))) "holds"  (Bool  "("  (Bool (Set (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "y")))  ($#r2_hidden :::"in"::: )  (Set (Var "D"))) & (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "R"))  ($#k1_wellord1 :::"-Seg"::: )  (Set (Var "y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "y")))  ")" )  ")" )  ")" )))) ; 
 
theorem :: WELLSET1:6 (Bool  "for" (Set (Var "N")) "being"    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "st"  (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  ) & (Bool (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R")))  ($#r1_hidden :::"="::: )  (Set (Var "N")))  ")" ))) ;