:: REALSET1  semantic presentation begin  
theorem :: REALSET1:1 (Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "X"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds"  (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))) ; 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "F" be   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "X")); mode  :::"Preserv":::  "of" "F" ->   ($#m1_subset_1 :::"Subset":::) "of" "X" means :: REALSET1:def 1 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) it "," it ($#k2_zfmisc_1 :::":]"::: ) ))) "holds"  (Bool (Set "F"  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r2_hidden :::"in"::: )  it)); end; 






:: deftheorem    defines :::"Preserv"::: REALSET1:def 1 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "b3")) "is"    ($#m1_realset1 :::"Preserv"::: )   "of" (Set (Var "F"))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "b3")) "," (Set (Var "b3")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds"  (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))))  ")" )))); 
 definitionlet "R" be   ($#m1_hidden :::"Relation":::); let "A" be    ($#m1_hidden :::"set"::: )  ; func "R" :::"||"::: "A" ->    ($#m1_hidden :::"set"::: )   equals :: REALSET1:def 2 (Set "R"  ($#k5_relat_1 :::"|"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) "A" "," "A" ($#k2_zfmisc_1 :::":]"::: ) )); end; 






:: deftheorem    defines :::"||"::: REALSET1:def 2 :  (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "R"))  ($#k1_realset1 :::"||"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "R"))  ($#k5_relat_1 :::"|"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) ))))); 
 registrationlet "R" be   ($#m1_hidden :::"Relation":::); let "A" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set "R"  ($#k1_realset1 :::"||"::: )  "A") ->   ($#v1_relat_1 :::"Relation-like"::: )   ; 
end; registrationlet "R" be   ($#m1_hidden :::"Function":::); let "A" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set "R"  ($#k1_realset1 :::"||"::: )  "A") ->   ($#v1_funct_1 :::"Function-like"::: )   ; 
end; 
theorem :: REALSET1:2 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "A")) "being"    ($#m1_realset1 :::"Preserv"::: )   "of" (Set (Var "F")) "holds"  (Bool (Set (Set (Var "F"))  ($#k1_realset1 :::"||"::: )  (Set (Var "A"))) "is"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")))))) ; 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "F" be   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "X")); let "A" be    ($#m1_realset1 :::"Preserv"::: )   "of" (Set (Const "F")); :: original: :::"||"::: redefine func "F" :::"||"::: "A" ->   ($#m1_subset_1 :::"BinOp":::) "of" "A"; end; 
theorem :: REALSET1:3 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Bool  "not" (Set (Var "X")) "is"   ($#v1_zfmisc_1 :::"trivial"::: )  )) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k6_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) "is"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ))  ")" )) ; 
 
theorem :: REALSET1:4 (Bool  "ex" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "st"  (Bool  "for" (Set (Var "z")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A")) "holds"  (Bool (Set (Set (Var "A"))  ($#k6_subset_1 :::"\"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "z")) ($#k6_domain_1 :::"}"::: ) )) "is"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ))) ; 
 definitionlet "X" be  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )    ($#m1_hidden :::"set"::: )  ; let "F" be   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "X")); let "x" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "X")); pred "F" :::"is_Bin_Op_Preserv"::: "x" means :: REALSET1:def 3 (Bool  "("  (Bool (Set "X"  ($#k6_subset_1 :::"\"::: )  (Set  ($#k6_domain_1 :::"{"::: ) "x" ($#k6_domain_1 :::"}"::: ) )) "is"    ($#m1_realset1 :::"Preserv"::: )   "of" "F") & (Bool (Set (Set  "(" "F"  ($#k1_realset1 :::"||"::: )  "X" ")" )  ($#k6_subset_1 :::"\"::: )  (Set  ($#k6_domain_1 :::"{"::: ) "x" ($#k6_domain_1 :::"}"::: ) )) "is"   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "(" "X"  ($#k6_subset_1 :::"\"::: )  (Set  ($#k6_domain_1 :::"{"::: ) "x" ($#k6_domain_1 :::"}"::: ) ) ")" ))  ")" ); end; 






:: deftheorem    defines :::"is_Bin_Op_Preserv"::: REALSET1:def 3 :  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "F"))  ($#r1_realset1 :::"is_Bin_Op_Preserv"::: )  (Set (Var "x"))) "iff" (Bool  "("  (Bool (Set (Set (Var "X"))  ($#k6_subset_1 :::"\"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) "is"    ($#m1_realset1 :::"Preserv"::: )   "of" (Set (Var "F"))) & (Bool (Set (Set  "(" (Set (Var "F"))  ($#k1_realset1 :::"||"::: )  (Set (Var "X")) ")" )  ($#k6_subset_1 :::"\"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )) "is"   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "(" (Set (Var "X"))  ($#k6_subset_1 :::"\"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" ))  ")" )  ")" )))); 
 
theorem :: REALSET1:5 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool  "ex" (Set (Var "F")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) "st"  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds"  (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))))))) ; 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "A" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); mode  :::"Presv":::  "of" "X" "," "A" ->   ($#m1_subset_1 :::"BinOp":::) "of" "X" means :: REALSET1:def 4 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) "A" "," "A" ($#k2_zfmisc_1 :::":]"::: ) ))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r2_hidden :::"in"::: )  "A")); end; 






:: deftheorem    defines :::"Presv"::: REALSET1:def 4 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "b3")) "is"    ($#m2_realset1 :::"Presv"::: )   "of" (Set (Var "X")) "," (Set (Var "A"))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))))  ")" )))); 
 
theorem :: REALSET1:6 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "F")) "being"    ($#m2_realset1 :::"Presv"::: )   "of" (Set (Var "X")) "," (Set (Var "A")) "holds"  (Bool (Set (Set (Var "F"))  ($#k1_realset1 :::"||"::: )  (Set (Var "A"))) "is"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")))))) ; 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "A" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); let "F" be    ($#m2_realset1 :::"Presv"::: )   "of" (Set (Const "X")) "," (Set (Const "A")); func "F" :::"|||"::: "A" ->   ($#m1_subset_1 :::"BinOp":::) "of" "A" equals :: REALSET1:def 5 (Set "F"  ($#k1_realset1 :::"||"::: )  "A"); end; 







:: deftheorem    defines :::"|||"::: REALSET1:def 5 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "F")) "being"    ($#m2_realset1 :::"Presv"::: )   "of" (Set (Var "X")) "," (Set (Var "A")) "holds"  (Bool (Set (Set (Var "F"))  ($#k3_realset1 :::"|||"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k1_realset1 :::"||"::: )  (Set (Var "A"))))))); 
 definitionlet "A" be    ($#m1_hidden :::"set"::: )  ; let "x" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "A")); mode  :::"DnT":::  "of" "x" "," "A" ->   ($#m1_subset_1 :::"BinOp":::) "of" "A" means :: REALSET1:def 6 (Bool  "for" (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "(" "A"  ($#k6_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set  "(" "A"  ($#k6_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "y")))  ($#r2_hidden :::"in"::: )  (Set "A"  ($#k6_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) )))); end; 






:: deftheorem    defines :::"DnT"::: REALSET1:def 6 :  (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set (Var "b3")) "is"    ($#m3_realset1 :::"DnT"::: )   "of" (Set (Var "x")) "," (Set (Var "A"))) "iff" (Bool  "for" (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "(" (Set (Var "A"))  ($#k6_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set  "(" (Set (Var "A"))  ($#k6_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y")))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k6_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))))  ")" )))); 
 
theorem :: REALSET1:7 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  (Bool  "for" (Set (Var "F")) "being"    ($#m3_realset1 :::"DnT"::: )   "of" (Set (Var "x")) "," (Set (Var "A")) "holds"  (Bool (Set (Set (Var "F"))  ($#k1_realset1 :::"||"::: )  (Set  "(" (Set (Var "A"))  ($#k6_subset_1 :::"\"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" )) "is"   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "(" (Set (Var "A"))  ($#k6_subset_1 :::"\"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" ))))) ; 
 definitionlet "A" be  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )    ($#m1_hidden :::"set"::: )  ; let "x" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "A")); let "F" be    ($#m3_realset1 :::"DnT"::: )   "of" (Set (Const "x")) "," (Set (Const "A")); func "F" :::"!":::  "(" "A" "," "x" ")"  ->   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "(" "A"  ($#k6_subset_1 :::"\"::: )  (Set  ($#k6_domain_1 :::"{"::: ) "x" ($#k6_domain_1 :::"}"::: ) ) ")" ) equals :: REALSET1:def 7 (Set "F"  ($#k1_realset1 :::"||"::: )  (Set  "(" "A"  ($#k6_subset_1 :::"\"::: )  (Set  ($#k6_domain_1 :::"{"::: ) "x" ($#k6_domain_1 :::"}"::: ) ) ")" )); end; 







:: deftheorem    defines :::"!"::: REALSET1:def 7 :  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  (Bool  "for" (Set (Var "F")) "being"    ($#m3_realset1 :::"DnT"::: )   "of" (Set (Var "x")) "," (Set (Var "A")) "holds"  (Bool (Set (Set (Var "F"))  ($#k4_realset1 :::"!"::: )   "(" (Set (Var "A")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k1_realset1 :::"||"::: )  (Set  "(" (Set (Var "A"))  ($#k6_subset_1 :::"\"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" )))))); 
 
theorem :: REALSET1:8 (Bool  "for" (Set (Var "F")) "being"  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Singleton":::) "of" (Set (Var "F")) "holds"  (Bool (Set (Set (Var "F"))  ($#k6_subset_1 :::"\"::: )  (Set (Var "A"))) "is"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ))) ; 
 registrationlet "F" be  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )    ($#m1_hidden :::"set"::: )  ; let "A" be   ($#m1_subset_1 :::"Singleton":::) "of" (Set (Const "F")); 
cluster (Set "F"  ($#k4_xboole_0 :::"\"::: )  "A") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end;