:: XBOOLE_1  semantic presentation begin  











theorem :: XBOOLE_1:1 (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"))) & (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Z")))) ; 
 
theorem :: XBOOLE_1:2 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Var "X")))) ; 
 
theorem :: XBOOLE_1:3 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: XBOOLE_1:4 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Z")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set (Var "Y"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Z")) ")" )))) ; 
 
theorem :: XBOOLE_1:5 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Z")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Z")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set (Var "Y"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Z")) ")" )))) ; 
 
theorem :: XBOOLE_1:6 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y"))))) ; 
 
theorem :: XBOOLE_1:7 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y"))))) ; 
 
theorem :: XBOOLE_1:8 (Bool  "for" (Set (Var "X")) "," (Set (Var "Z")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Z"))) & (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")))  ($#r1_tarski :::"c="::: )  (Set (Var "Z")))) ; 
 
theorem :: XBOOLE_1:9 (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 (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Z")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "Y"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Z"))))) ; 
 
theorem :: XBOOLE_1:10 (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 (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "Z"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y"))))) ; 
 
theorem :: XBOOLE_1:11 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")))  ($#r1_tarski :::"c="::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Z")))) ; 
 
theorem :: XBOOLE_1:12 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set (Var "Y")))) ; 
 
theorem :: XBOOLE_1:13 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "V")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y"))) & (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set (Var "V")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Z")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "Y"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "V"))))) ; 
 
theorem :: XBOOLE_1:14 (Bool  "for" (Set (Var "Y")) "," (Set (Var "X")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "X"))) & (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "V")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "V"))) & (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set (Var "V")))) "holds"  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "V")))  ")" )) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "Y"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Z"))))) ; 
 
theorem :: XBOOLE_1:15 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: XBOOLE_1:16 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set  "(" (Set (Var "Y"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z")) ")" )))) ; 
 
theorem :: XBOOLE_1:17 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))) ; 
 
theorem :: XBOOLE_1:18 (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 (Set (Var "Y"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z"))))) "holds"  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) ; 
 
theorem :: XBOOLE_1:19 (Bool  "for" (Set (Var "Z")) "," (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set (Var "X"))) & (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y"))))) ; 
 
theorem :: XBOOLE_1:20 (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"))) & (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Z"))) & (Bool  "("   "for" (Set (Var "V")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "V"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y"))) & (Bool (Set (Var "V"))  ($#r1_tarski :::"c="::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Var "V"))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))  ")" )) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "Y"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z"))))) ; 
 
theorem :: XBOOLE_1:21 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "X")))) ; 
 
theorem :: XBOOLE_1:22 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "X")))) ; 
 
theorem :: XBOOLE_1:23 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set  "(" (Set (Var "Y"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z")) ")" )))) ; 
 
theorem :: XBOOLE_1:24 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set (Var "Y"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Z")) ")" )))) ; 
 
theorem :: XBOOLE_1:25 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set (Var "Y"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z")) ")" ) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set (Var "Z"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set  "(" (Set (Var "Y"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Z")) ")" ) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set  "(" (Set (Var "Z"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "X")) ")" )))) ; 
 
theorem :: XBOOLE_1:26 (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 (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "Y"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z"))))) ; 
 
theorem :: XBOOLE_1:27 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "V")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y"))) & (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set (Var "V")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "Y"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "V"))))) ; 
 
theorem :: XBOOLE_1:28 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set (Var "X")))) ; 
 
theorem :: XBOOLE_1:29 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Z"))))) ; 
 
theorem :: XBOOLE_1:30 (Bool  "for" (Set (Var "X")) "," (Set (Var "Z")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set (Var "Y"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z"))))) ; 
 
theorem :: XBOOLE_1:31 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z")) ")" ))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "Y"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Z"))))) ; 
 
theorem :: XBOOLE_1:32 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "Y"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "X"))))) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set (Var "Y")))) ; 
 
theorem :: XBOOLE_1:33 (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 (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Z")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "Y"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Z"))))) ; 
 
theorem :: XBOOLE_1:34 (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 (Set (Set (Var "Z"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "Z"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "X"))))) ; 
 
theorem :: XBOOLE_1:35 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "V")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y"))) & (Bool (Set (Var "Z"))  ($#r1_tarski :::"c="::: )  (Set (Var "V")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "V")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "Y"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Z"))))) ; 
 
theorem :: XBOOLE_1:36 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y")))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))) ; 
 
theorem :: XBOOLE_1:37 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "iff" (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))  ")" )) ; 
 
theorem :: XBOOLE_1:38 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "Y"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "X"))))) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: XBOOLE_1:39 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set (Var "Y"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y"))))) ; 
 
theorem :: XBOOLE_1:40 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" )  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y"))))) ; 
 
theorem :: XBOOLE_1:41 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y")) ")" )  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Z")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set  "(" (Set (Var "Y"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Z")) ")" )))) ; 
 
theorem :: XBOOLE_1:42 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" )  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Z")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Z")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set (Var "Y"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Z")) ")" )))) ; 
 
theorem :: XBOOLE_1:43 (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 (Set (Var "Y"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Z"))))) "holds"  (Bool (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y")))  ($#r1_tarski :::"c="::: )  (Set (Var "Z")))) ; 
 
theorem :: XBOOLE_1:44 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y")))  ($#r1_tarski :::"c="::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "Y"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Z"))))) ; 
 
theorem :: XBOOLE_1:45 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Var "Y"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set (Var "Y"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "X")) ")" )))) ; 
 
theorem :: XBOOLE_1:46 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: XBOOLE_1:47 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y"))))) ; 
 
theorem :: XBOOLE_1:48 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set  "(" (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y"))))) ; 
 
theorem :: XBOOLE_1:49 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set  "(" (Set (Var "Y"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" )  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Z"))))) ; 
 
theorem :: XBOOLE_1:50 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set  "(" (Set (Var "Y"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" )  ($#k4_xboole_0 :::"\"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z")) ")" )))) ; 
 
theorem :: XBOOLE_1:51 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "X")))) ; 
 
theorem :: XBOOLE_1:52 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set  "(" (Set (Var "Y"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z")) ")" )))) ; 
 
theorem :: XBOOLE_1:53 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set  "(" (Set (Var "Y"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y")) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set  "(" (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Z")) ")" )))) ; 
 
theorem :: XBOOLE_1:54 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set  "(" (Set (Var "Y"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Z")) ")" )))) ; 
 
theorem :: XBOOLE_1:55 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" )  ($#k4_xboole_0 :::"\"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set (Var "Y"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "X")) ")" )))) ; 
 
theorem :: XBOOLE_1:56 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r2_xboole_0 :::"c<"::: )  (Set (Var "Y"))) & (Bool (Set (Var "Y"))  ($#r2_xboole_0 :::"c<"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Var "X"))  ($#r2_xboole_0 :::"c<"::: )  (Set (Var "Z")))) ; 
 
theorem :: XBOOLE_1:57 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("   "not" (Bool (Set (Var "X"))  ($#r2_xboole_0 :::"c<"::: )  (Set (Var "Y"))) "or"  "not" (Bool (Set (Var "Y"))  ($#r2_xboole_0 :::"c<"::: )  (Set (Var "X")))  ")" )) ; 
 
theorem :: XBOOLE_1:58 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r2_xboole_0 :::"c<"::: )  (Set (Var "Y"))) & (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Var "X"))  ($#r2_xboole_0 :::"c<"::: )  (Set (Var "Z")))) ; 
 
theorem :: XBOOLE_1:59 (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"))) & (Bool (Set (Var "Y"))  ($#r2_xboole_0 :::"c<"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Var "X"))  ($#r2_xboole_0 :::"c<"::: )  (Set (Var "Z")))) ; 
 
theorem :: XBOOLE_1:60 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool  "not" (Bool (Set (Var "Y"))  ($#r2_xboole_0 :::"c<"::: )  (Set (Var "X"))))) ; 
 
theorem :: XBOOLE_1:61 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_xboole_0 :::"c<"::: )  (Set (Var "X")))) ; 
 
theorem :: XBOOLE_1:62 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "holds" (Bool (Bool  "not" (Set (Var "X"))  ($#r2_xboole_0 :::"c<"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))) ; 
 
theorem :: XBOOLE_1:63 (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"))) & (Bool (Set (Var "Y"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Z")))) ; 
 
theorem :: XBOOLE_1:64 (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"))) & (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B")))) ; 
 
theorem :: XBOOLE_1:65 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: XBOOLE_1:66 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "X"))) "iff" (Bool (Set (Var "X"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )) ; 
 
theorem :: XBOOLE_1:67 (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"))) & (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Z"))) & (Bool (Set (Var "Y"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: XBOOLE_1:68 (Bool  "for" (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y"))) & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Var "Y"))  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "Z"))))) ; 
 
theorem :: XBOOLE_1:69 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "Y"))))) ; 
 
theorem :: XBOOLE_1:70 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "Y"))) "or" (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "Z")))  ")" ) "iff" (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"meets"::: )  (Set (Set (Var "Y"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Z"))))  ")" )) ; 
 
theorem :: XBOOLE_1:71 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "Z"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")))) & (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Y"))) & (Bool (Set (Var "Z"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set (Var "Z")))) ; 
 
theorem :: XBOOLE_1:72 (Bool  "for" (Set (Var "X9")) "," (Set (Var "Y9")) "," (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Set (Var "X9"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y9")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")))) & (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "X9"))) & (Bool (Set (Var "Y"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Y9")))) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set (Var "Y9")))) ; 
 
theorem :: XBOOLE_1:73 (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 (Set (Var "Y"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Z")))) & (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) ; 
 
theorem :: XBOOLE_1:74 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"meets"::: )  (Set (Set (Var "Y"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z"))))) "holds"  (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "Y")))) ; 
 
theorem :: XBOOLE_1:75 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")))  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "Y")))) ; 
 
theorem :: XBOOLE_1:76 (Bool  "for" (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Y"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")))  ($#r1_xboole_0 :::"misses"::: )  (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z"))))) ; 
 
theorem :: XBOOLE_1:77 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "Y"))) & (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"meets"::: )  (Set (Set (Var "Y"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z"))))) ; 
 
theorem :: XBOOLE_1:78 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set  "(" (Set (Var "Y"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z"))))) ; 
 
theorem :: XBOOLE_1:79 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y")))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Y")))) ; 
 
theorem :: XBOOLE_1:80 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Set (Var "Y"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Z"))))) ; 
 
theorem :: XBOOLE_1:81 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Set (Var "Y"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Z"))))) "holds"  (Bool (Set (Var "Y"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Z"))))) ; 
 
theorem :: XBOOLE_1:82 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y")))  ($#r1_xboole_0 :::"misses"::: )  (Set (Set (Var "Y"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "X"))))) ; 
 
theorem :: XBOOLE_1:83 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Y"))) "iff" (Bool (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set (Var "X")))  ")" )) ; 
 
theorem :: XBOOLE_1:84 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "Y"))) & (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"meets"::: )  (Set (Set (Var "Y"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Z"))))) ; 
 
theorem :: XBOOLE_1:85 (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 (Set (Var "X"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Set (Var "Z"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y"))))) ; 
 
theorem :: XBOOLE_1:86 (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"))) & (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "Y"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Z"))))) ; 
 
theorem :: XBOOLE_1:87 (Bool  "for" (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Y"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Z")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Z")) ")" )  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y"))))) ; 
 
theorem :: XBOOLE_1:88 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" )  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set (Var "X")))) ; 
 
theorem :: XBOOLE_1:89 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")))  ($#r1_xboole_0 :::"misses"::: )  (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y"))))) ; 
 
theorem :: XBOOLE_1:90 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" ))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Y")))) ; 
 
theorem :: XBOOLE_1:91 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k5_xboole_0 :::"\+\"::: )  (Set (Var "Y")) ")" )  ($#k5_xboole_0 :::"\+\"::: )  (Set (Var "Z")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k5_xboole_0 :::"\+\"::: )  (Set  "(" (Set (Var "Y"))  ($#k5_xboole_0 :::"\+\"::: )  (Set (Var "Z")) ")" )))) ; 
 
theorem :: XBOOLE_1:92 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k5_xboole_0 :::"\+\"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: XBOOLE_1:93 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k5_xboole_0 :::"\+\"::: )  (Set (Var "Y")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" )))) ; 
 
theorem :: XBOOLE_1:94 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k5_xboole_0 :::"\+\"::: )  (Set (Var "Y")) ")" )  ($#k5_xboole_0 :::"\+\"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" )))) ; 
 
theorem :: XBOOLE_1:95 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k5_xboole_0 :::"\+\"::: )  (Set (Var "Y")) ")" )  ($#k5_xboole_0 :::"\+\"::: )  (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" )))) ; 
 
theorem :: XBOOLE_1:96 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "X"))  ($#k5_xboole_0 :::"\+\"::: )  (Set (Var "Y"))))) ; 
 
theorem :: XBOOLE_1:97 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y")))  ($#r1_tarski :::"c="::: )  (Set (Var "Z"))) & (Bool (Set (Set (Var "Y"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set (Var "Z")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k5_xboole_0 :::"\+\"::: )  (Set (Var "Y")))  ($#r1_tarski :::"c="::: )  (Set (Var "Z")))) ; 
 
theorem :: XBOOLE_1:98 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k5_xboole_0 :::"\+\"::: )  (Set  "(" (Set (Var "Y"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "X")) ")" )))) ; 
 
theorem :: XBOOLE_1:99 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k5_xboole_0 :::"\+\"::: )  (Set (Var "Y")) ")" )  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Z")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set  "(" (Set (Var "Y"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Z")) ")" ) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set (Var "Y"))  ($#k4_xboole_0 :::"\"::: )  (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Z")) ")" ) ")" )))) ; 
 
theorem :: XBOOLE_1:100 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k5_xboole_0 :::"\+\"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" )))) ; 
 
theorem :: XBOOLE_1:101 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k5_xboole_0 :::"\+\"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" )  ($#k4_xboole_0 :::"\"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" )))) ; 
 
theorem :: XBOOLE_1:102 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set  "(" (Set (Var "Y"))  ($#k5_xboole_0 :::"\+\"::: )  (Set (Var "Z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set  "(" (Set (Var "Y"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Z")) ")" ) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z")) ")" )))) ; 
 
theorem :: XBOOLE_1:103 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")))  ($#r1_xboole_0 :::"misses"::: )  (Set (Set (Var "X"))  ($#k5_xboole_0 :::"\+\"::: )  (Set (Var "Y"))))) ; 
 
theorem :: XBOOLE_1:104 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "X"))  ($#r2_xboole_0 :::"c<"::: )  (Set (Var "Y"))) "or" (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set (Var "Y"))) "or" (Bool (Set (Var "Y"))  ($#r2_xboole_0 :::"c<"::: )  (Set (Var "X")))  ")" ) "iff" (Bool (Set (Var "X")) "," (Set (Var "Y"))  ($#r3_xboole_0 :::"are_c=-comparable"::: )  )  ")" )) ; 
 begin  
theorem :: XBOOLE_1:105 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r2_xboole_0 :::"c<"::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Set (Var "Y"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "X")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: XBOOLE_1:106 (Bool  "for" (Set (Var "X")) "," (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "A"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "B"))))) "holds"  (Bool  "("  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "A"))) & (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B")))  ")" )) ; 
 
theorem :: XBOOLE_1:107 (Bool  "for" (Set (Var "X")) "," (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "A"))  ($#k5_xboole_0 :::"\+\"::: )  (Set (Var "B")))) "iff" (Bool  "("  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "A"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "B")))) & (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Set (Var "A"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "B"))))  ")" )  ")" )) ; 
 
theorem :: XBOOLE_1:108 (Bool  "for" (Set (Var "X")) "," (Set (Var "A")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))) ; 
 
theorem :: XBOOLE_1:109 (Bool  "for" (Set (Var "X")) "," (Set (Var "A")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y")))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))) ; 
 
theorem :: XBOOLE_1:110 (Bool  "for" (Set (Var "X")) "," (Set (Var "A")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "A"))) & (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k5_xboole_0 :::"\+\"::: )  (Set (Var "Y")))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))) ; 
 
theorem :: XBOOLE_1:111 (Bool  "for" (Set (Var "X")) "," (Set (Var "Z")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z")) ")" )  ($#k4_xboole_0 :::"\"::: )  (Set  "(" (Set (Var "Y"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "Y")) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z"))))) ; 
 
theorem :: XBOOLE_1:112 (Bool  "for" (Set (Var "X")) "," (Set (Var "Z")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z")) ")" )  ($#k5_xboole_0 :::"\+\"::: )  (Set  "(" (Set (Var "Y"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k5_xboole_0 :::"\+\"::: )  (Set (Var "Y")) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z"))))) ; 
 
theorem :: XBOOLE_1:113 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "V")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Z")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "V")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set  "(" (Set (Var "Y"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Z")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "V")) ")" )))) ; 
 
theorem :: XBOOLE_1:114 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "D"))) & (Bool (Set (Var "B"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "D"))) & (Bool (Set (Var "C"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "D")))) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "B")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "C")))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "D")))) ; 
 
theorem :: XBOOLE_1:115 (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )    "holds" (Bool (Bool  "not" (Set (Var "A"))  ($#r2_xboole_0 :::"c<"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))) ; 
 
theorem :: XBOOLE_1:116 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set  "(" (Set (Var "Y"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Z")) ")" )))) ; 
 
theorem :: XBOOLE_1:117 (Bool  "for" (Set (Var "P")) "," (Set (Var "G")) "," (Set (Var "C")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "C"))  ($#r1_tarski :::"c="::: )  (Set (Var "G")))) "holds"  (Bool (Set (Set (Var "P"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "P"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "G")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set (Var "P"))  ($#k3_xboole_0 :::"/\"::: )  (Set  "(" (Set (Var "G"))  ($#k4_xboole_0 :::"\"::: )  (Set (Var "C")) ")" ) ")" )))) ;