:: ZFMISC_1  semantic presentation begin  






















registrationlet "x", "y" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set  ($#k4_tarski :::"["::: ) "x" "," "y" ($#k4_tarski :::"]"::: ) ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; func  :::"bool"::: "X" ->    ($#m1_hidden :::"set"::: )   means :: ZFMISC_1:def 1 (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "Z"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  "X")  ")" )); end; 





:: deftheorem    defines :::"bool"::: ZFMISC_1:def 1 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b2")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set (Var "X")))) "iff" (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "Z"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) "iff" (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))  ")" ))  ")" ))); 
 definitionlet "X1", "X2" be    ($#m1_hidden :::"set"::: )  ; func :::"[:":::"X1" "," "X2":::":]"::: ->    ($#m1_hidden :::"set"::: )   means :: ZFMISC_1:def 2 (Bool  "for" (Set (Var "z")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "ex" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "X1") & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  "X2") & (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ))  ")" ))  ")" )); end; 






:: deftheorem    defines :::"[:"::: ZFMISC_1:def 2 :  (Bool  "for" (Set (Var "X1")) "," (Set (Var "X2")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b3")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) ($#k2_zfmisc_1 :::":]"::: ) )) "iff" (Bool  "for" (Set (Var "z")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))) "iff" (Bool  "ex" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X1"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X2"))) & (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ))  ")" ))  ")" ))  ")" ))); 
 definitionlet "X1", "X2", "X3" be    ($#m1_hidden :::"set"::: )  ; func :::"[:":::"X1" "," "X2" "," "X3":::":]"::: ->    ($#m1_hidden :::"set"::: )   equals :: ZFMISC_1:def 3 (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k2_zfmisc_1 :::"[:"::: ) "X1" "," "X2" ($#k2_zfmisc_1 :::":]"::: ) ) "," "X3" ($#k2_zfmisc_1 :::":]"::: ) ); end; 







:: deftheorem    defines :::"[:"::: ZFMISC_1:def 3 :  (Bool  "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set  ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k3_zfmisc_1 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "X3")) ($#k2_zfmisc_1 :::":]"::: ) ))); 
 definitionlet "X1", "X2", "X3", "X4" be    ($#m1_hidden :::"set"::: )  ; func :::"[:":::"X1" "," "X2" "," "X3" "," "X4":::":]"::: ->    ($#m1_hidden :::"set"::: )   equals :: ZFMISC_1:def 4 (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k3_zfmisc_1 :::"[:"::: ) "X1" "," "X2" "," "X3" ($#k3_zfmisc_1 :::":]"::: ) ) "," "X4" ($#k2_zfmisc_1 :::":]"::: ) ); end; 








:: deftheorem    defines :::"[:"::: ZFMISC_1:def 4 :  (Bool  "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set  ($#k4_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "," (Set (Var "X4")) ($#k4_zfmisc_1 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k3_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) ($#k3_zfmisc_1 :::":]"::: ) ) "," (Set (Var "X4")) ($#k2_zfmisc_1 :::":]"::: ) ))); 
 begin  
theorem :: ZFMISC_1:1 (Bool (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) ; 
 
theorem :: ZFMISC_1:2 (Bool (Set   ($#k3_tarski :::"union"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) ; 
 
theorem :: ZFMISC_1:3 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#r1_tarski :::"c="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))) ; 
 
theorem :: ZFMISC_1:4 (Bool  "for" (Set (Var "x")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k2_tarski :::"}"::: ) ))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y1")))) ; 
 
theorem :: ZFMISC_1:5 (Bool  "for" (Set (Var "x")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k2_tarski :::"}"::: ) ))) "holds"  (Bool (Set (Var "y1"))  ($#r1_hidden :::"="::: )  (Set (Var "y2")))) ; 
 
theorem :: ZFMISC_1:6 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("   "not" (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k2_tarski :::"}"::: ) )) "or" (Bool (Set (Var "x1"))  ($#r1_hidden :::"="::: )  (Set (Var "y1"))) "or" (Bool (Set (Var "x1"))  ($#r1_hidden :::"="::: )  (Set (Var "y2")))  ")" )) ; 
 
theorem :: ZFMISC_1:7 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#r1_tarski :::"c="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ))) ; 
 
theorem :: ZFMISC_1:8 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))) ; 
 
theorem :: ZFMISC_1:9 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ))) ; 
 
theorem :: ZFMISC_1:10 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#r1_xboole_0 :::"misses"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y")))) ; 
 
theorem :: ZFMISC_1:11 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y")))) "holds"  (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#r1_xboole_0 :::"misses"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: ZFMISC_1:12 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#k3_xboole_0 :::"/\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))) ; 
 
theorem :: ZFMISC_1:13 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#k3_xboole_0 :::"/\"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: ZFMISC_1:14 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#k4_xboole_0 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) "iff" (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y")))  ")" )) ; 
 
theorem :: ZFMISC_1:15 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#k4_xboole_0 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))) ; 
 
theorem :: ZFMISC_1:16 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#k4_xboole_0 :::"\"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: ZFMISC_1:17 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y")))) "holds"  (Bool (Set (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#k4_xboole_0 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: ZFMISC_1:18 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#r1_tarski :::"c="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))) ; 
 
theorem :: ZFMISC_1:19 (Bool  "for" (Set (Var "z")) "," (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("   "not" (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "z")) ($#k1_tarski :::"}"::: ) )  ($#r1_tarski :::"c="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )) "or" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) "or" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))  ")" )) ; 
 
theorem :: ZFMISC_1:20 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r1_tarski :::"c="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "z")) ($#k1_tarski :::"}"::: ) ))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "z")))) ; 
 
theorem :: ZFMISC_1:21 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r1_tarski :::"c="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "z")) ($#k1_tarski :::"}"::: ) ))) "holds"  (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "z")) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: ZFMISC_1:22 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("   "not" (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) )  ($#r1_tarski :::"c="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k2_tarski :::"}"::: ) )) "or" (Bool (Set (Var "x1"))  ($#r1_hidden :::"="::: )  (Set (Var "y1"))) "or" (Bool (Set (Var "x1"))  ($#r1_hidden :::"="::: )  (Set (Var "y2")))  ")" )) ; 
 
theorem :: ZFMISC_1:23 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y")))) "holds"  (Bool (Set (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#k5_xboole_0 :::"\+\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ))) ; 
 
theorem :: ZFMISC_1:24 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#k2_tarski :::"}"::: ) ))) ; 
 
theorem :: ZFMISC_1:25 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "x")))) ; 
 
theorem :: ZFMISC_1:26 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) ($#k2_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ))) ; 
 
theorem :: ZFMISC_1:27 canceled; 
 
theorem :: ZFMISC_1:28 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "x1")) "," (Set (Var "y1")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y1")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "x1"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "y1")))  ")" )  ")" )) ; 
 
theorem :: ZFMISC_1:29 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: ZFMISC_1:30 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k2_tarski :::"{"::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k2_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) )) & (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "z")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) ))  ")" )) ; 
 
theorem :: ZFMISC_1:31 (Bool  "for" (Set (Var "x")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#r1_tarski :::"c="::: )  (Set (Var "X"))) "iff" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  ")" )) ; 
 
theorem :: ZFMISC_1:32 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) )  ($#r1_tarski :::"c="::: )  (Set (Var "Z"))) "iff" (Bool  "("  (Bool (Set (Var "x1"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z"))) & (Bool (Set (Var "x2"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))  ")" )  ")" )) ; 
 
theorem :: ZFMISC_1:33 (Bool  "for" (Set (Var "Y")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) "iff" (Bool  "("  (Bool (Set (Var "Y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "or" (Bool (Set (Var "Y"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))  ")" )  ")" )) ; 
 
theorem :: ZFMISC_1:34 (Bool  "for" (Set (Var "Y")) "," (Set (Var "X")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "X"))) & (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))))) "holds"  (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )))) ; 
 
theorem :: ZFMISC_1:35 (Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"<>"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Var "X"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "ex" (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x")))  ")" ))) ; 
 
theorem :: ZFMISC_1:36 (Bool  "for" (Set (Var "Z")) "," (Set (Var "x1")) "," (Set (Var "x2")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) )) "iff" (Bool  "("  (Bool (Set (Var "Z"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "or" (Bool (Set (Var "Z"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) )) "or" (Bool (Set (Var "Z"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x2")) ($#k1_tarski :::"}"::: ) )) "or" (Bool (Set (Var "Z"))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ))  ")" )  ")" )) ; 
 
theorem :: ZFMISC_1:37 (Bool  "for" (Set (Var "z")) "," (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("   "not" (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "z")) ($#k1_tarski :::"}"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")))) "or" (Bool  "("  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "z")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Var "Y"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "z")) ($#k1_tarski :::"}"::: ) ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "Y"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "z")) ($#k1_tarski :::"}"::: ) ))  ")" ) "or" (Bool  "("  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "z")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Var "Y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )  ")" )) ; 
 
theorem :: ZFMISC_1:38 (Bool  "for" (Set (Var "z")) "," (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "z")) ($#k1_tarski :::"}"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")))) & (Bool (Set (Var "X"))  ($#r1_hidden :::"<>"::: )  (Set (Var "Y"))) & (Bool (Bool  "not" (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))) "holds"  (Bool (Set (Var "Y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: ZFMISC_1:39 (Bool  "for" (Set (Var "x")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) ; 
 
theorem :: ZFMISC_1:40 (Bool  "for" (Set (Var "x")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Var "X")))) ; 
 
theorem :: ZFMISC_1:41 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Z")))  ($#r1_tarski :::"c="::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) ; 
 
theorem :: ZFMISC_1:42 (Bool  "for" (Set (Var "x")) "," (Set (Var "Z")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Z")))  ($#r1_hidden :::"="::: )  (Set (Var "Z")))) ; 
 
theorem :: ZFMISC_1:43 (Bool  "for" (Set (Var "x")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "holds" (Bool (Set (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "X")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: ZFMISC_1:44 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "holds" (Bool (Set (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "X")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: ZFMISC_1:45 (Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) ; 
 
theorem :: ZFMISC_1:46 (Bool  "for" (Set (Var "x")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: ZFMISC_1:47 (Bool  "for" (Set (Var "x")) "," (Set (Var "Z")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ))) ; 
 
theorem :: ZFMISC_1:48 (Bool  "for" (Set (Var "x")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "X")))) "holds"  (Bool  "not" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))) ; 
 
theorem :: ZFMISC_1:49 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Z")))) "holds"  (Bool  "not" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z"))))) ; 
 
theorem :: ZFMISC_1:50 (Bool  "for" (Set (Var "x")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))) "holds"  (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "X")))) ; 
 
theorem :: ZFMISC_1:51 (Bool  "for" (Set (Var "x")) "," (Set (Var "Z")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) & (Bool (Bool  "not" (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z"))))) "holds"  (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Z")))) ; 
 
theorem :: ZFMISC_1:52 (Bool  "for" (Set (Var "x")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("  (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "X"))) "or" (Bool (Set (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))  ")" )) ; 
 
theorem :: ZFMISC_1:53 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("   "not" (Bool (Set (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) "or"  "not" (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))  ")" )) ; 
 
theorem :: ZFMISC_1:54 (Bool  "for" (Set (Var "x")) "," (Set (Var "X")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool  "("   "not" (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))  ")" )) "holds"  (Bool (Set (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: ZFMISC_1:55 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ))) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) ; 
 
theorem :: ZFMISC_1:56 (Bool  "for" (Set (Var "z")) "," (Set (Var "X")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) "iff" (Bool  "("  (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "z"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x")))  ")" )  ")" )) ; 
 
theorem :: ZFMISC_1:57 (Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) "iff" (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))  ")" )) ; 
 
theorem :: ZFMISC_1:58 (Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("   "not" (Bool (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "or" (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "or" (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))  ")" )) ; 
 
theorem :: ZFMISC_1:59 (Bool  "for" (Set (Var "x")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#k4_xboole_0 :::"\"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) "iff" (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))  ")" )) ; 
 
theorem :: ZFMISC_1:60 (Bool  "for" (Set (Var "x")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#k4_xboole_0 :::"\"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "iff" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  ")" )) ; 
 
theorem :: ZFMISC_1:61 (Bool  "for" (Set (Var "x")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("  (Bool (Set (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#k4_xboole_0 :::"\"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "or" (Bool (Set (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#k4_xboole_0 :::"\"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))  ")" )) ; 
 
theorem :: ZFMISC_1:62 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#k4_xboole_0 :::"\"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) "iff" (Bool  "("  (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) & (Bool  "("  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))  ")" )  ")" )  ")" )) ; 
 
theorem :: ZFMISC_1:63 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#k4_xboole_0 :::"\"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )) "iff" (Bool  "("  (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) & (Bool (Bool  "not" (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))  ")" )  ")" )) ; 
 
theorem :: ZFMISC_1:64 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#k4_xboole_0 :::"\"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))  ")" )  ")" )) ; 
 
theorem :: ZFMISC_1:65 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("  (Bool (Set (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#k4_xboole_0 :::"\"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "or" (Bool (Set (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#k4_xboole_0 :::"\"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) "or" (Bool (Set (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#k4_xboole_0 :::"\"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )) "or" (Bool (Set (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#k4_xboole_0 :::"\"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ))  ")" )) ; 
 
theorem :: ZFMISC_1:66 (Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "iff" (Bool  "("  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "or" (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) "or" (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )) "or" (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ))  ")" )  ")" )) ; 
 
theorem :: ZFMISC_1:67 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "B")))) "holds"  (Bool (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set (Var "A")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set (Var "B"))))) ; 
 
theorem :: ZFMISC_1:68 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "A")) ($#k1_tarski :::"}"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set (Var "A"))))) ; 
 
theorem :: ZFMISC_1:69 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set (Var "A")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set (Var "B")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "(" (Set (Var "A"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "B")) ")" )))) ; 
 
theorem :: ZFMISC_1:70 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set (Var "A")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "(" (Set (Var "A"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "B")) ")" )))) "holds"  (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r3_xboole_0 :::"are_c=-comparable"::: )  )) ; 
 
theorem :: ZFMISC_1:71 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "(" (Set (Var "A"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set (Var "A")) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set (Var "B")) ")" )))) ; 
 
theorem :: ZFMISC_1:72 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "(" (Set (Var "A"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "B")) ")" ))  ($#r1_tarski :::"c="::: )  (Set (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set (Var "A")) ")" )  ($#k4_xboole_0 :::"\"::: )  (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set (Var "B")) ")" ) ")" )))) ; 
 
theorem :: ZFMISC_1:73 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set  "(" (Set (Var "A"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "B")) ")" ) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set  "(" (Set (Var "B"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "A")) ")" ) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "(" (Set (Var "A"))  ($#k5_xboole_0 :::"\+\"::: )  (Set (Var "B")) ")" )))) ; 
 
theorem :: ZFMISC_1:74 (Bool  "for" (Set (Var "X")) "," (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "A"))))) ; 
 
theorem :: ZFMISC_1:75 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y"))))) ; 
 
theorem :: ZFMISC_1:76 (Bool  "for" (Set (Var "A")) "," (Set (Var "Z")) "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 "A")))) "holds"  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Z")))  ")" )) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "A")))  ($#r1_tarski :::"c="::: )  (Set (Var "Z")))) ; 
 
theorem :: ZFMISC_1:77 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "B")))) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "A")))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "B"))))) ; 
 
theorem :: ZFMISC_1:78 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set  "(" (Set (Var "A"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "A")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "B")) ")" )))) ; 
 
theorem :: ZFMISC_1:79 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set  "(" (Set (Var "A"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "B")) ")" ))  ($#r1_tarski :::"c="::: )  (Set (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "A")) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "B")) ")" )))) ; 
 
theorem :: ZFMISC_1:80 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "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 "A")))) "holds"  (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B")))  ")" )) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "A")))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B")))) ; 
 
theorem :: ZFMISC_1:81 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "A")))) ; 
 
theorem :: ZFMISC_1:82 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "A")) ")" )))) ; 
 
theorem :: ZFMISC_1:83 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"<>"::: )  (Set (Var "Y"))) & (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "B")))) & (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "A"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "B"))))) "holds"  (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Y")))  ")" )) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set  "(" (Set (Var "A"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "A")) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "B")) ")" )))) ; 
 
theorem :: ZFMISC_1:84 (Bool  "for" (Set (Var "A")) "," (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool  "ex" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))) & (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ))  ")" ))) ; 
 
theorem :: ZFMISC_1:85 (Bool  "for" (Set (Var "z")) "," (Set (Var "X1")) "," (Set (Var "Y1")) "," (Set (Var "X2")) "," (Set (Var "Y2")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "Y1")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k3_xboole_0 :::"/\"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X2")) "," (Set (Var "Y2")) ($#k2_zfmisc_1 :::":]"::: ) )))) "holds"  (Bool  "ex" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "X1"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "X2")))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "Y1"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y2"))))  ")" ))) ; 
 
theorem :: ZFMISC_1:86 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" ) ")" )))) ; 
 
theorem :: ZFMISC_1:87 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))  ")" )  ")" )) ; 
 
theorem :: ZFMISC_1:88 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "," (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  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ))) ; 
 
theorem :: ZFMISC_1:89 (Bool  "for" (Set (Var "X1")) "," (Set (Var "Y1")) "," (Set (Var "X2")) "," (Set (Var "Y2")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "Y1")) ($#k2_zfmisc_1 :::":]"::: ) )) "iff" (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X2")) "," (Set (Var "Y2")) ($#k2_zfmisc_1 :::":]"::: ) ))  ")" )  ")" )) "holds"  (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "Y1")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X2")) "," (Set (Var "Y2")) ($#k2_zfmisc_1 :::":]"::: ) ))) ; 
 
theorem :: ZFMISC_1:90 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "iff" (Bool  "("  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "or" (Bool (Set (Var "Y"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )  ")" )) ; 
 
theorem :: ZFMISC_1:91 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "Y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set (Var "Y")))) ; 
 
theorem :: ZFMISC_1:92 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set (Var "Y")))) ; 
 
theorem :: ZFMISC_1:93 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: ZFMISC_1:94 (Bool  "for" (Set (Var "Z")) "," (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Z"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool  "("  (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_tarski :::"c="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) )) "or" (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Z")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_tarski :::"c="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Z")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))  ")" )) "holds"  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) ; 
 
theorem :: ZFMISC_1:95 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool  "("  (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_tarski :::"c="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Z")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_tarski :::"c="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Z")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))  ")" )) ; 
 
theorem :: ZFMISC_1:96 (Bool  "for" (Set (Var "X1")) "," (Set (Var "Y1")) "," (Set (Var "X2")) "," (Set (Var "Y2")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X1"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y1"))) & (Bool (Set (Var "X2"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y2")))) "holds"  (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_tarski :::"c="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y1")) "," (Set (Var "Y2")) ($#k2_zfmisc_1 :::":]"::: ) ))) ; 
 
theorem :: ZFMISC_1:97 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" ) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) ))) & (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Z")) "," (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Z")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Z")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )))  ")" )) ; 
 
theorem :: ZFMISC_1:98 (Bool  "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "(" (Set (Var "X1"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "X2")) ")" ) "," (Set  "(" (Set (Var "Y1"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y2")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "Y1")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "Y2")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X2")) "," (Set (Var "Y1")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X2")) "," (Set (Var "Y2")) ($#k2_zfmisc_1 :::":]"::: ) )))) ; 
 
theorem :: ZFMISC_1:99 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" ) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k3_xboole_0 :::"/\"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) ))) & (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Z")) "," (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Z")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k3_xboole_0 :::"/\"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Z")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )))  ")" )) ; 
 
theorem :: ZFMISC_1:100 (Bool  "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "(" (Set (Var "X1"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "X2")) ")" ) "," (Set  "(" (Set (Var "Y1"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y2")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "Y1")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k3_xboole_0 :::"/\"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X2")) "," (Set (Var "Y2")) ($#k2_zfmisc_1 :::":]"::: ) )))) ; 
 
theorem :: ZFMISC_1:101 (Bool  "for" (Set (Var "A")) "," (Set (Var "X")) "," (Set (Var "B")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "X"))) & (Bool (Set (Var "B"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k3_xboole_0 :::"/\"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ))) ; 
 
theorem :: ZFMISC_1:102 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "(" (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y")) ")" ) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k4_xboole_0 :::"\"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) ))) & (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Z")) "," (Set  "(" (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Z")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k4_xboole_0 :::"\"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Z")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )))  ")" )) ; 
 
theorem :: ZFMISC_1:103 (Bool  "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k4_xboole_0 :::"\"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y1")) "," (Set (Var "Y2")) ($#k2_zfmisc_1 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "(" (Set (Var "X1"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y1")) ")" ) "," (Set (Var "X2")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set  "(" (Set (Var "X2"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y2")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )))) ; 
 
theorem :: ZFMISC_1:104 (Bool  "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("  (Bool (Set (Var "X1"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "X2"))) "or" (Bool (Set (Var "Y1"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Y2")))  ")" )) "holds"  (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "Y1")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_xboole_0 :::"misses"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X2")) "," (Set (Var "Y2")) ($#k2_zfmisc_1 :::":]"::: ) ))) ; 
 
theorem :: ZFMISC_1:105 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set (Var "z")) ($#k1_tarski :::"}"::: ) ) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "z"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))  ")" )  ")" )) ; 
 
theorem :: ZFMISC_1:106 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "," (Set (Var "z")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "z")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "z")))  ")" )  ")" )) ; 
 
theorem :: ZFMISC_1:107 (Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "("  (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )) ; 
 
theorem :: ZFMISC_1:108 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y")))) "holds"  (Bool  "("  (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_xboole_0 :::"misses"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_xboole_0 :::"misses"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))  ")" )) ; 
 
theorem :: ZFMISC_1:109 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ))) & (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )))  ")" )) ; 
 
theorem :: ZFMISC_1:110 (Bool  "for" (Set (Var "X1")) "," (Set (Var "Y1")) "," (Set (Var "X2")) "," (Set (Var "Y2")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X1"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "Y1"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "Y1")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X2")) "," (Set (Var "Y2")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds"  (Bool  "("  (Bool (Set (Var "X1"))  ($#r1_hidden :::"="::: )  (Set (Var "X2"))) & (Bool (Set (Var "Y1"))  ($#r1_hidden :::"="::: )  (Set (Var "Y2")))  ")" )) ; 
 
theorem :: ZFMISC_1:111 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) "or" (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ))  ")" )) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: ZFMISC_1:112 (Bool  "for" (Set (Var "N")) "being"    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "M")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "N"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool  "("   "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))  ")" ) & (Bool  "("   "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) "holds"  (Bool (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))  ")" ) & (Bool  "("   "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("   "not" (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "M"))) "or" (Bool (Set (Var "X")) "," (Set (Var "M"))  ($#r2_tarski :::"are_equipotent"::: )  ) "or" (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))  ")" )  ")" )  ")" ))) ; 
 








theorem :: ZFMISC_1:113 (Bool  "for" (Set (Var "e")) "," (Set (Var "X1")) "," (Set (Var "Y1")) "," (Set (Var "X2")) "," (Set (Var "Y2")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "Y1")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X2")) "," (Set (Var "Y2")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds"  (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "(" (Set (Var "X1"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "X2")) ")" ) "," (Set  "(" (Set (Var "Y1"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y2")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))) ; 
 begin  
theorem :: ZFMISC_1:114 (Bool  "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_tarski :::"c="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y1")) "," (Set (Var "Y2")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Var "X1"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y1"))) & (Bool (Set (Var "X2"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y2")))  ")" )) ; 
 
theorem :: ZFMISC_1:115 (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("  (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_tarski :::"c="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "C")) "," (Set (Var "D")) ($#k2_zfmisc_1 :::":]"::: ) )) "or" (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "B")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_tarski :::"c="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "C")) ($#k2_zfmisc_1 :::":]"::: ) ))  ")" )) "holds"  (Bool (Set (Var "B"))  ($#r1_tarski :::"c="::: )  (Set (Var "D"))))) ; 
 
theorem :: ZFMISC_1:116 (Bool  "for" (Set (Var "x")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "X")))) ; 
 
theorem :: ZFMISC_1:117 (Bool  "for" (Set (Var "x")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" )  ($#k4_xboole_0 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "X")))) ; 
 
theorem :: ZFMISC_1:118 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set  ($#k1_enumset1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k1_enumset1 :::"}"::: ) )) "iff" (Bool  "("  (Bool (Set (Var "Z"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "or" (Bool (Set (Var "Z"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) "or" (Bool (Set (Var "Z"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )) "or" (Bool (Set (Var "Z"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "z")) ($#k1_tarski :::"}"::: ) )) "or" (Bool (Set (Var "Z"))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )) "or" (Bool (Set (Var "Z"))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k2_tarski :::"}"::: ) )) "or" (Bool (Set (Var "Z"))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k2_tarski :::"}"::: ) )) "or" (Bool (Set (Var "Z"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_enumset1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k1_enumset1 :::"}"::: ) ))  ")" )  ")" )) ; 
 
theorem :: ZFMISC_1:119 (Bool  "for" (Set (Var "N")) "," (Set (Var "M")) "," (Set (Var "X1")) "," (Set (Var "Y1")) "," (Set (Var "X2")) "," (Set (Var "Y2")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "N"))  ($#r1_tarski :::"c="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "Y1")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Var "M"))  ($#r1_tarski :::"c="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X2")) "," (Set (Var "Y2")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds"  (Bool (Set (Set (Var "N"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "M")))  ($#r1_tarski :::"c="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "(" (Set (Var "X1"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "X2")) ")" ) "," (Set  "(" (Set (Var "Y1"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y2")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))) ; 
 
theorem :: ZFMISC_1:120 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) & (Bool (Bool  "not" (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )))) ; 
 
theorem :: ZFMISC_1:121 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) & (Bool (Bool  "not" (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) ")" )  ($#k4_xboole_0 :::"\"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )))) ; 
 definitionlet "x1", "x2", "x3" be    ($#m1_hidden :::"set"::: )  ; pred "x1" "," "x2" "," "x3" :::"are_mutually_different":::  means :: ZFMISC_1:def 5 (Bool  "("  (Bool "x1"  ($#r1_hidden :::"<>"::: )  "x2") & (Bool "x1"  ($#r1_hidden :::"<>"::: )  "x3") & (Bool "x2"  ($#r1_hidden :::"<>"::: )  "x3")  ")" ); end; 






:: deftheorem    defines :::"are_mutually_different"::: ZFMISC_1:def 5 :  (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3"))  ($#r1_zfmisc_1 :::"are_mutually_different"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x2"))) & (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x3"))) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x3")))  ")" )  ")" )); 
 definitionlet "x1", "x2", "x3", "x4" be    ($#m1_hidden :::"set"::: )  ; pred "x1" "," "x2" "," "x3" "," "x4" :::"are_mutually_different":::  means :: ZFMISC_1:def 6 (Bool  "("  (Bool "x1"  ($#r1_hidden :::"<>"::: )  "x2") & (Bool "x1"  ($#r1_hidden :::"<>"::: )  "x3") & (Bool "x1"  ($#r1_hidden :::"<>"::: )  "x4") & (Bool "x2"  ($#r1_hidden :::"<>"::: )  "x3") & (Bool "x2"  ($#r1_hidden :::"<>"::: )  "x4") & (Bool "x3"  ($#r1_hidden :::"<>"::: )  "x4")  ")" ); end; 







:: deftheorem    defines :::"are_mutually_different"::: ZFMISC_1:def 6 :  (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4"))  ($#r2_zfmisc_1 :::"are_mutually_different"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x2"))) & (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x3"))) & (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x4"))) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x3"))) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x4"))) & (Bool (Set (Var "x3"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x4")))  ")" )  ")" )); 
 definitionlet "x1", "x2", "x3", "x4", "x5" be    ($#m1_hidden :::"set"::: )  ; pred "x1" "," "x2" "," "x3" "," "x4" "," "x5" :::"are_mutually_different":::  means :: ZFMISC_1:def 7 (Bool  "("  (Bool "x1"  ($#r1_hidden :::"<>"::: )  "x2") & (Bool "x1"  ($#r1_hidden :::"<>"::: )  "x3") & (Bool "x1"  ($#r1_hidden :::"<>"::: )  "x4") & (Bool "x1"  ($#r1_hidden :::"<>"::: )  "x5") & (Bool "x2"  ($#r1_hidden :::"<>"::: )  "x3") & (Bool "x2"  ($#r1_hidden :::"<>"::: )  "x4") & (Bool "x2"  ($#r1_hidden :::"<>"::: )  "x5") & (Bool "x3"  ($#r1_hidden :::"<>"::: )  "x4") & (Bool "x3"  ($#r1_hidden :::"<>"::: )  "x5") & (Bool "x4"  ($#r1_hidden :::"<>"::: )  "x5")  ")" ); end; 








:: deftheorem    defines :::"are_mutually_different"::: ZFMISC_1:def 7 :  (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5"))  ($#r3_zfmisc_1 :::"are_mutually_different"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x2"))) & (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x3"))) & (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x4"))) & (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x5"))) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x3"))) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x4"))) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x5"))) & (Bool (Set (Var "x3"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x4"))) & (Bool (Set (Var "x3"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x5"))) & (Bool (Set (Var "x4"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x5")))  ")" )  ")" )); 
 definitionlet "x1", "x2", "x3", "x4", "x5", "x6" be    ($#m1_hidden :::"set"::: )  ; pred "x1" "," "x2" "," "x3" "," "x4" "," "x5" "," "x6" :::"are_mutually_different":::  means :: ZFMISC_1:def 8 (Bool  "("  (Bool "x1"  ($#r1_hidden :::"<>"::: )  "x2") & (Bool "x1"  ($#r1_hidden :::"<>"::: )  "x3") & (Bool "x1"  ($#r1_hidden :::"<>"::: )  "x4") & (Bool "x1"  ($#r1_hidden :::"<>"::: )  "x5") & (Bool "x1"  ($#r1_hidden :::"<>"::: )  "x6") & (Bool "x2"  ($#r1_hidden :::"<>"::: )  "x3") & (Bool "x2"  ($#r1_hidden :::"<>"::: )  "x4") & (Bool "x2"  ($#r1_hidden :::"<>"::: )  "x5") & (Bool "x2"  ($#r1_hidden :::"<>"::: )  "x6") & (Bool "x3"  ($#r1_hidden :::"<>"::: )  "x4") & (Bool "x3"  ($#r1_hidden :::"<>"::: )  "x5") & (Bool "x3"  ($#r1_hidden :::"<>"::: )  "x6") & (Bool "x4"  ($#r1_hidden :::"<>"::: )  "x5") & (Bool "x4"  ($#r1_hidden :::"<>"::: )  "x6") & (Bool "x5"  ($#r1_hidden :::"<>"::: )  "x6")  ")" ); end; 









:: deftheorem    defines :::"are_mutually_different"::: ZFMISC_1:def 8 :  (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6"))  ($#r4_zfmisc_1 :::"are_mutually_different"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x2"))) & (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x3"))) & (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x4"))) & (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x5"))) & (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x6"))) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x3"))) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x4"))) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x5"))) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x6"))) & (Bool (Set (Var "x3"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x4"))) & (Bool (Set (Var "x3"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x5"))) & (Bool (Set (Var "x3"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x6"))) & (Bool (Set (Var "x4"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x5"))) & (Bool (Set (Var "x4"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x6"))) & (Bool (Set (Var "x5"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x6")))  ")" )  ")" )); 
 definitionlet "x1", "x2", "x3", "x4", "x5", "x6", "x7" be    ($#m1_hidden :::"set"::: )  ; pred "x1" "," "x2" "," "x3" "," "x4" "," "x5" "," "x6" "," "x7" :::"are_mutually_different":::  means :: ZFMISC_1:def 9 (Bool  "("  (Bool "x1"  ($#r1_hidden :::"<>"::: )  "x2") & (Bool "x1"  ($#r1_hidden :::"<>"::: )  "x3") & (Bool "x1"  ($#r1_hidden :::"<>"::: )  "x4") & (Bool "x1"  ($#r1_hidden :::"<>"::: )  "x5") & (Bool "x1"  ($#r1_hidden :::"<>"::: )  "x6") & (Bool "x1"  ($#r1_hidden :::"<>"::: )  "x7") & (Bool "x2"  ($#r1_hidden :::"<>"::: )  "x3") & (Bool "x2"  ($#r1_hidden :::"<>"::: )  "x4") & (Bool "x2"  ($#r1_hidden :::"<>"::: )  "x5") & (Bool "x2"  ($#r1_hidden :::"<>"::: )  "x6") & (Bool "x2"  ($#r1_hidden :::"<>"::: )  "x7") & (Bool "x3"  ($#r1_hidden :::"<>"::: )  "x4") & (Bool "x3"  ($#r1_hidden :::"<>"::: )  "x5") & (Bool "x3"  ($#r1_hidden :::"<>"::: )  "x6") & (Bool "x3"  ($#r1_hidden :::"<>"::: )  "x7") & (Bool "x4"  ($#r1_hidden :::"<>"::: )  "x5") & (Bool "x4"  ($#r1_hidden :::"<>"::: )  "x6") & (Bool "x4"  ($#r1_hidden :::"<>"::: )  "x7") & (Bool "x5"  ($#r1_hidden :::"<>"::: )  "x6") & (Bool "x5"  ($#r1_hidden :::"<>"::: )  "x7") & (Bool "x6"  ($#r1_hidden :::"<>"::: )  "x7")  ")" ); end; 










:: deftheorem    defines :::"are_mutually_different"::: ZFMISC_1:def 9 :  (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7"))  ($#r5_zfmisc_1 :::"are_mutually_different"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x2"))) & (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x3"))) & (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x4"))) & (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x5"))) & (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x6"))) & (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x7"))) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x3"))) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x4"))) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x5"))) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x6"))) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x7"))) & (Bool (Set (Var "x3"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x4"))) & (Bool (Set (Var "x3"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x5"))) & (Bool (Set (Var "x3"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x6"))) & (Bool (Set (Var "x3"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x7"))) & (Bool (Set (Var "x4"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x5"))) & (Bool (Set (Var "x4"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x6"))) & (Bool (Set (Var "x4"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x7"))) & (Bool (Set (Var "x5"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x6"))) & (Bool (Set (Var "x5"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x7"))) & (Bool (Set (Var "x6"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x7")))  ")" )  ")" )); 
 
theorem :: ZFMISC_1:122 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ) "," (Set  ($#k2_tarski :::"{"::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k2_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k2_enumset1 :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k4_tarski :::"]"::: ) ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "x2")) "," (Set (Var "y1")) ($#k4_tarski :::"]"::: ) ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "x2")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ) ($#k2_enumset1 :::"}"::: ) ))) ; 
 
theorem :: ZFMISC_1:123 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y")))) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" )  ($#k4_xboole_0 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "A"))  ($#k4_xboole_0 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )))) ; 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; attr "X" is  :::"trivial":::  means :: ZFMISC_1:def 10 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "X") & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  "X")) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))); end; 




:: deftheorem    defines :::"trivial"::: ZFMISC_1:def 10 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v1_zfmisc_1 :::"trivial"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y"))))  ")" )); 
 registration
cluster   ($#v1_xboole_0 :::"empty"::: )    ->   ($#v1_zfmisc_1 :::"trivial"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registration
cluster  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )   ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "x" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set  ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ) ->   ($#v1_zfmisc_1 :::"trivial"::: )   ; 
end; registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_zfmisc_1 :::"trivial"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: ZFMISC_1:124 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "p")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "B"))) & (Bool (Set (Set (Var "B"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "p")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Set (Var "A"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "p")) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: ZFMISC_1:125 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "p")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Set (Var "A"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "B")))  ($#r1_tarski :::"c="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "p")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "C"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "A"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "C")))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B")))) ; 
 
theorem :: ZFMISC_1:126 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Var "x"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "y")))  ")" )) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "A")))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "B"))))) ; 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; let "Y" be   ($#v1_xboole_0 :::"empty"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set  ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) ) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; registrationlet "X" be   ($#v1_xboole_0 :::"empty"::: )     ($#m1_hidden :::"set"::: )  ; let "Y" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set  ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) ) ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; 
theorem :: ZFMISC_1:127 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )    "holds" (Bool (Bool  "not" (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) )))) ; 
 
theorem :: ZFMISC_1:128 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) ; 
 
theorem :: ZFMISC_1:129 (Bool  "for" (Set (Var "B")) "," (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds"  (Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#k4_tarski :::"]"::: ) ))  ")" ))) ; 
 
theorem :: ZFMISC_1:130 (Bool  "for" (Set (Var "B")) "," (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "B"))  ($#r1_tarski :::"c="::: )  (Set (Var "A"))) & (Bool (Set (Var "A")) "is"   ($#v1_zfmisc_1 :::"trivial"::: )  )) "holds"  (Bool (Set (Var "B")) "is"   ($#v1_zfmisc_1 :::"trivial"::: )  )) ; 
 registration
cluster  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )   for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: ZFMISC_1:131 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Bool  "not" (Set (Var "X")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Set (Var "X")) "is"   ($#v1_zfmisc_1 :::"trivial"::: )  )) "holds"  (Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )))) ; 
 
theorem :: ZFMISC_1:132 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#v1_zfmisc_1 :::"trivial"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )))) ; 
 
theorem :: ZFMISC_1:133 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set  ($#k1_enumset1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k1_enumset1 :::"}"::: ) )  ($#r1_tarski :::"c="::: )  (Set (Var "X")))) ; 
 
theorem :: ZFMISC_1:134 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"union"::: )  (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "X")) ")" ))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"union"::: )  (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "X")) ")" )))  ")" )) ; 
 
theorem :: ZFMISC_1:135 (Bool  "for" (Set (Var "Y")) "," (Set (Var "x")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("   "not" (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "Y"))  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) "or" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) "or" (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))  ")" )) ; 
 
theorem :: ZFMISC_1:136 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))  ")" )  ")" )) ; 
 
theorem :: ZFMISC_1:137 (Bool  "for" (Set (Var "x")) "," (Set (Var "Y")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))  ($#r1_tarski :::"c="::: )  (Set (Var "Y"))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))) & (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))  ")" )  ")" )) ; 
 
theorem :: ZFMISC_1:138 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "B"))) & (Bool (Set (Var "B"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "A"))  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ))) & (Bool (Bool  "not" (Set (Set (Var "A"))  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "B"))))) "holds"  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "B")))) ;