:: XBOOLE_0  semantic presentation begin  







scheme  :: XBOOLE_0:sch 1 Separation{ F1() ->    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" )) & (Bool P1[(Set (Var "x"))])  ")" )  ")" )))
 proof 


end; definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; attr "X" is  :::"empty":::  means :: XBOOLE_0:def 1 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "holds" (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "X"))); end; 




:: deftheorem    defines :::"empty"::: XBOOLE_0:def 1 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v1_xboole_0 :::"empty"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "holds" (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))))  ")" )); 
 registration
cluster   ($#v1_xboole_0 :::"empty"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; definitionfunc  :::"{}":::  ->    ($#m1_hidden :::"set"::: )   equals :: XBOOLE_0:def 2  "the"   ($#v1_xboole_0 :::"empty"::: )     ($#m1_hidden :::"set"::: )  ; let "X", "Y" be    ($#m1_hidden :::"set"::: )  ; func "X" :::"\/"::: "Y" ->    ($#m1_hidden :::"set"::: )   means :: XBOOLE_0:def 3 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "X") "or" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "Y")  ")" )  ")" )); commutativity  
(Bool  "for" (Set (Var "b1")) "," (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b1"))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) "or" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))  ")" )  ")" )  ")" )) "holds"  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b1"))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))) "or" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  ")" )  ")" )))
 ; idempotence  
(Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) "or" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  ")" )  ")" ))
 ; func "X" :::"/\"::: "Y" ->    ($#m1_hidden :::"set"::: )   means :: XBOOLE_0:def 4 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "X") & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "Y")  ")" )  ")" )); commutativity  
(Bool  "for" (Set (Var "b1")) "," (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b1"))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))  ")" )  ")" )  ")" )) "holds"  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b1"))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  ")" )  ")" )))
 ; idempotence  
(Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  ")" )  ")" ))
 ; func "X" :::"\"::: "Y" ->    ($#m1_hidden :::"set"::: )   means :: XBOOLE_0:def 5 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "X") & (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "Y"))  ")" )  ")" )); end; 






















:: deftheorem    defines :::"{}"::: XBOOLE_0:def 2 :  (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r1_hidden :::"="::: )   "the"   ($#v1_xboole_0 :::"empty"::: )     ($#m1_hidden :::"set"::: )  ); 
 
:: deftheorem    defines :::"\/"::: XBOOLE_0:def 3 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "b3")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) "or" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))  ")" )  ")" ))  ")" )); 
 
:: deftheorem    defines :::"/\"::: XBOOLE_0:def 4 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "b3")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))  ")" )  ")" ))  ")" )); 
 
:: deftheorem    defines :::"\"::: XBOOLE_0:def 5 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "b3")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y")))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))))  ")" )  ")" ))  ")" )); 
 definitionlet "X", "Y" be    ($#m1_hidden :::"set"::: )  ; func "X" :::"\+\"::: "Y" ->    ($#m1_hidden :::"set"::: )   equals :: XBOOLE_0:def 6 (Set (Set  "(" "X"  ($#k4_xboole_0 :::"\"::: )  "Y" ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" "Y"  ($#k4_xboole_0 :::"\"::: )  "X" ")" )); commutativity  
(Bool  "for" (Set (Var "b1")) "," (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set (Var "Y"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "X")) ")" )))) "holds"  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "Y"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "X")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y")) ")" ))))
 ; pred "X" :::"misses"::: "Y" means :: XBOOLE_0:def 7 (Bool (Set "X"  ($#k3_xboole_0 :::"/\"::: )  "Y")  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )); symmetry  
(Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set (Set (Var "Y"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))
 ; pred "X" :::"c<"::: "Y" means :: XBOOLE_0:def 8 (Bool  "("  (Bool "X"  ($#r1_tarski :::"c="::: )  "Y") & (Bool "X"  ($#r1_hidden :::"<>"::: )  "Y")  ")" ); irreflexivity  
(Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("   "not" (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "X"))) "or"  "not" (Bool (Set (Var "X"))  ($#r1_hidden :::"<>"::: )  (Set (Var "X")))  ")" ))
 ; asymmetry  
(Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y"))) & (Bool (Set (Var "X"))  ($#r1_hidden :::"<>"::: )  (Set (Var "Y"))) & (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))) "holds"  (Bool  "not" (Bool (Set (Var "Y"))  ($#r1_hidden :::"<>"::: )  (Set (Var "X")))))
 ; pred "X" "," "Y" :::"are_c=-comparable":::  means :: XBOOLE_0:def 9 (Bool  "("  (Bool "X"  ($#r1_tarski :::"c="::: )  "Y") "or" (Bool "Y"  ($#r1_tarski :::"c="::: )  "X")  ")" ); reflexivity  
(Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "X"))) "or" (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))  ")" ))
 ; symmetry  
(Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("  (Bool  "("  (Bool (Bool  "not" (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) & (Bool (Bool  "not" (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "X"))))  ")" ) "or" (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "X"))) "or" (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))  ")" ))
 ; redefine pred "X" :::"="::: "Y" means :: XBOOLE_0:def 10 (Bool  "("  (Bool "X"  ($#r1_tarski :::"c="::: )  "Y") & (Bool "Y"  ($#r1_tarski :::"c="::: )  "X")  ")" ); end; 


























:: deftheorem    defines :::"\+\"::: XBOOLE_0:def 6 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k5_xboole_0 :::"\+\"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set (Var "Y"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "X")) ")" )))); 
 
:: deftheorem    defines :::"misses"::: XBOOLE_0:def 7 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Y"))) "iff" (Bool (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )); 
 
:: deftheorem    defines :::"c<"::: XBOOLE_0:def 8 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r2_xboole_0 :::"c<"::: )  (Set (Var "Y"))) "iff" (Bool  "("  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y"))) & (Bool (Set (Var "X"))  ($#r1_hidden :::"<>"::: )  (Set (Var "Y")))  ")" )  ")" )); 
 
:: deftheorem    defines :::"are_c=-comparable"::: XBOOLE_0:def 9 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X")) "," (Set (Var "Y"))  ($#r3_xboole_0 :::"are_c=-comparable"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y"))) "or" (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))  ")" )  ")" )); 
 
:: deftheorem    defines :::"="::: XBOOLE_0:def 10 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set (Var "Y"))) "iff" (Bool  "("  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y"))) & (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))  ")" )  ")" )); 
 notationlet "X", "Y" be    ($#m1_hidden :::"set"::: )  ; antonym "X" :::"meets"::: "Y" for "X" :::"misses"::: "Y"; end; 
theorem :: XBOOLE_0:1 (Bool  "for" (Set (Var "x")) "," (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "X"))  ($#k5_xboole_0 :::"\+\"::: )  (Set (Var "Y")))) "iff" (Bool  "("  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))))  ")" ) "or" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))) & (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))  ")" )  ")" )  ")" )) ; 
 
theorem :: XBOOLE_0:2 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))) "iff" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))  ")" )  ")" )  ")" )) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "Y"))  ($#k5_xboole_0 :::"\+\"::: )  (Set (Var "Z"))))) ; 
 registration
cluster (Set   ($#k1_xboole_0 :::"{}"::: )  ) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; registrationlet "x1" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set  ($#k1_tarski :::"{"::: ) "x1" ($#k1_tarski :::"}"::: ) ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
let "x2" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set  ($#k2_tarski :::"{"::: ) "x1" "," "x2" ($#k2_tarski :::"}"::: ) ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set "D"  ($#k2_xboole_0 :::"\/"::: )  "X") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 

cluster (Set "X"  ($#k2_xboole_0 :::"\/"::: )  "D") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: XBOOLE_0:3 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "Y"))) "iff" (Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))  ")" ))  ")" )) ; 
 
theorem :: XBOOLE_0:4 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "Y"))) "iff" (Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")))))  ")" )) ; 
 
theorem :: XBOOLE_0:5 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Y"))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")))) & (Bool  "not" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))))  ")" ))) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))) & (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))  ")" )) ; 
 scheme  :: XBOOLE_0:sch 2 Extensionality{ F1() ->    ($#m1_hidden :::"set"::: )  , F2() ->    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool (Set F1 "("  ")" )  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" ))
 provided
(Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" )) "iff" (Bool P1[(Set (Var "x"))])  ")" ))
 and  
(Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set F2 "("  ")" )) "iff" (Bool P1[(Set (Var "x"))])  ")" ))
 proof 


end; scheme  :: XBOOLE_0:sch 3 SetEq{ P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "X1")) "," (Set (Var "X2")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X1"))) "iff" (Bool P1[(Set (Var "x"))])  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X2"))) "iff" (Bool P1[(Set (Var "x"))])  ")" )  ")" )) "holds"  (Bool (Set (Var "X1"))  ($#r1_hidden :::"="::: )  (Set (Var "X2"))))
 proof 


end; begin  
theorem :: XBOOLE_0:6 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r2_xboole_0 :::"c<"::: )  (Set (Var "Y")))) "holds"  (Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))) & (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))  ")" ))) ; 
 
theorem :: XBOOLE_0:7 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))) ;