:: MBOOLEAN  semantic presentation begin  










definitionlet "I" be    ($#m1_hidden :::"set"::: )  ; let "A" be   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); func  :::"bool"::: "A" ->   ($#m1_hidden :::"ManySortedSet":::) "of" "I" means :: MBOOLEAN:def 1 (Bool  "for" (Set (Var "i")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  "I")) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "(" "A"  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" )))); end; 






:: deftheorem    defines :::"bool"::: MBOOLEAN:def 1 :  (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "b3")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_mboolean :::"bool"::: )  (Set (Var "A")))) "iff" (Bool  "for" (Set (Var "i")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set (Var "I")))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "(" (Set (Var "A"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" ))))  ")" ))); 
 registrationlet "I" be    ($#m1_hidden :::"set"::: )  ; let "A" be   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); 
cluster (Set   ($#k1_mboolean :::"bool"::: )  "A") -> bbbadV2_RELAT_1() ; 
end; 
theorem :: MBOOLEAN:1 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r6_pboole :::"="::: )  (Set   ($#k1_mboolean :::"bool"::: )  (Set (Var "Y")))) "iff" (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds"   (Bool  "("  (Bool (Set (Var "A"))  ($#r1_pboole :::"in"::: )  (Set (Var "X"))) "iff" (Bool (Set (Var "A"))  ($#r2_pboole :::"c="::: )  (Set (Var "Y")))  ")" ))  ")" ))) ; 
 
theorem :: MBOOLEAN:2 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_mboolean :::"bool"::: )  (Set  "("  ($#k1_pboole :::"[[0]]"::: )  (Set (Var "I")) ")" ))  ($#r6_pboole :::"="::: )  (Set (Set (Var "I"))  ($#k7_funcop_1 :::"-->"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )))) ; 
 
theorem :: MBOOLEAN:3 (Bool  "for" (Set (Var "I")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_mboolean :::"bool"::: )  (Set  "(" (Set (Var "I"))  ($#k7_funcop_1 :::"-->"::: )  (Set (Var "x")) ")" ))  ($#r6_pboole :::"="::: )  (Set (Set (Var "I"))  ($#k7_funcop_1 :::"-->"::: )  (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set (Var "x")) ")" )))) ; 
 
theorem :: MBOOLEAN:4 (Bool  "for" (Set (Var "I")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_mboolean :::"bool"::: )  (Set  "(" (Set (Var "I"))  ($#k7_funcop_1 :::"-->"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ))  ($#r6_pboole :::"="::: )  (Set (Set (Var "I"))  ($#k7_funcop_1 :::"-->"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#k2_tarski :::"}"::: ) )))) ; 
 
theorem :: MBOOLEAN:5 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds"  (Bool (Set   ($#k1_pboole :::"[[0]]"::: )  (Set (Var "I")))  ($#r2_pboole :::"c="::: )  (Set (Var "A"))))) ; 
 
theorem :: MBOOLEAN:6 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool (Set (Var "A"))  ($#r2_pboole :::"c="::: )  (Set (Var "B")))) "holds"  (Bool (Set   ($#k1_mboolean :::"bool"::: )  (Set (Var "A")))  ($#r2_pboole :::"c="::: )  (Set   ($#k1_mboolean :::"bool"::: )  (Set (Var "B")))))) ; 
 
theorem :: MBOOLEAN:7 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds"  (Bool (Set (Set  "("  ($#k1_mboolean :::"bool"::: )  (Set (Var "A")) ")" )  ($#k2_pboole :::"\/"::: )  (Set  "("  ($#k1_mboolean :::"bool"::: )  (Set (Var "B")) ")" ))  ($#r2_pboole :::"c="::: )  (Set   ($#k1_mboolean :::"bool"::: )  (Set  "(" (Set (Var "A"))  ($#k2_pboole :::"\/"::: )  (Set (Var "B")) ")" ))))) ; 
 
theorem :: MBOOLEAN:8 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool (Set (Set  "("  ($#k1_mboolean :::"bool"::: )  (Set (Var "A")) ")" )  ($#k2_pboole :::"\/"::: )  (Set  "("  ($#k1_mboolean :::"bool"::: )  (Set (Var "B")) ")" ))  ($#r6_pboole :::"="::: )  (Set   ($#k1_mboolean :::"bool"::: )  (Set  "(" (Set (Var "A"))  ($#k2_pboole :::"\/"::: )  (Set (Var "B")) ")" )))) "holds"  (Bool  "for" (Set (Var "i")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set (Var "I")))) "holds"  (Bool (Set (Set (Var "A"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i"))) "," (Set (Set (Var "B"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r3_xboole_0 :::"are_c=-comparable"::: )  )))) ; 
 
theorem :: MBOOLEAN:9 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds"  (Bool (Set   ($#k1_mboolean :::"bool"::: )  (Set  "(" (Set (Var "A"))  ($#k3_pboole :::"/\"::: )  (Set (Var "B")) ")" ))  ($#r6_pboole :::"="::: )  (Set (Set  "("  ($#k1_mboolean :::"bool"::: )  (Set (Var "A")) ")" )  ($#k3_pboole :::"/\"::: )  (Set  "("  ($#k1_mboolean :::"bool"::: )  (Set (Var "B")) ")" ))))) ; 
 
theorem :: MBOOLEAN:10 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds"  (Bool (Set   ($#k1_mboolean :::"bool"::: )  (Set  "(" (Set (Var "A"))  ($#k4_pboole :::"\"::: )  (Set (Var "B")) ")" ))  ($#r2_pboole :::"c="::: )  (Set (Set  "(" (Set (Var "I"))  ($#k7_funcop_1 :::"-->"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" )  ($#k2_pboole :::"\/"::: )  (Set  "(" (Set  "("  ($#k1_mboolean :::"bool"::: )  (Set (Var "A")) ")" )  ($#k4_pboole :::"\"::: )  (Set  "("  ($#k1_mboolean :::"bool"::: )  (Set (Var "B")) ")" ) ")" ))))) ; 
 
theorem :: MBOOLEAN:11 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "," (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r2_pboole :::"c="::: )  (Set (Set (Var "A"))  ($#k4_pboole :::"\"::: )  (Set (Var "B")))) "iff" (Bool  "("  (Bool (Set (Var "X"))  ($#r2_pboole :::"c="::: )  (Set (Var "A"))) & (Bool (Set (Var "X"))  ($#r5_pboole :::"misses"::: )  (Set (Var "B")))  ")" )  ")" ))) ; 
 
theorem :: MBOOLEAN:12 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds"  (Bool (Set (Set  "("  ($#k1_mboolean :::"bool"::: )  (Set  "(" (Set (Var "A"))  ($#k4_pboole :::"\"::: )  (Set (Var "B")) ")" ) ")" )  ($#k2_pboole :::"\/"::: )  (Set  "("  ($#k1_mboolean :::"bool"::: )  (Set  "(" (Set (Var "B"))  ($#k4_pboole :::"\"::: )  (Set (Var "A")) ")" ) ")" ))  ($#r2_pboole :::"c="::: )  (Set   ($#k1_mboolean :::"bool"::: )  (Set  "(" (Set (Var "A"))  ($#k5_pboole :::"\+\"::: )  (Set (Var "B")) ")" ))))) ; 
 
theorem :: MBOOLEAN:13 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "," (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r2_pboole :::"c="::: )  (Set (Set (Var "A"))  ($#k5_pboole :::"\+\"::: )  (Set (Var "B")))) "iff" (Bool  "("  (Bool (Set (Var "X"))  ($#r2_pboole :::"c="::: )  (Set (Set (Var "A"))  ($#k2_pboole :::"\/"::: )  (Set (Var "B")))) & (Bool (Set (Var "X"))  ($#r5_pboole :::"misses"::: )  (Set (Set (Var "A"))  ($#k3_pboole :::"/\"::: )  (Set (Var "B"))))  ")" )  ")" ))) ; 
 
theorem :: MBOOLEAN:14 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "," (Set (Var "A")) "," (Set (Var "Y")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool  "("  (Bool (Set (Var "X"))  ($#r2_pboole :::"c="::: )  (Set (Var "A"))) "or" (Bool (Set (Var "Y"))  ($#r2_pboole :::"c="::: )  (Set (Var "A")))  ")" )) "holds"  (Bool (Set (Set (Var "X"))  ($#k3_pboole :::"/\"::: )  (Set (Var "Y")))  ($#r2_pboole :::"c="::: )  (Set (Var "A"))))) ; 
 
theorem :: MBOOLEAN:15 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "," (Set (Var "A")) "," (Set (Var "Y")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool (Set (Var "X"))  ($#r2_pboole :::"c="::: )  (Set (Var "A")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k4_pboole :::"\"::: )  (Set (Var "Y")))  ($#r2_pboole :::"c="::: )  (Set (Var "A"))))) ; 
 
theorem :: MBOOLEAN:16 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "," (Set (Var "A")) "," (Set (Var "Y")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool (Set (Var "X"))  ($#r2_pboole :::"c="::: )  (Set (Var "A"))) & (Bool (Set (Var "Y"))  ($#r2_pboole :::"c="::: )  (Set (Var "A")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k5_pboole :::"\+\"::: )  (Set (Var "Y")))  ($#r2_pboole :::"c="::: )  (Set (Var "A"))))) ; 
 
theorem :: MBOOLEAN:17 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds"  (Bool (Set  ($#k6_pboole :::"[|"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k6_pboole :::"|]"::: ) )  ($#r2_pboole :::"c="::: )  (Set   ($#k1_mboolean :::"bool"::: )  (Set  "("  ($#k1_mboolean :::"bool"::: )  (Set  "(" (Set (Var "X"))  ($#k2_pboole :::"\/"::: )  (Set (Var "Y")) ")" ) ")" ))))) ; 
 
theorem :: MBOOLEAN:18 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "," (Set (Var "A")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds"   (Bool  "("  (Bool (Set (Var "X"))  ($#r2_pboole :::"c="::: )  (Set (Var "A"))) "iff" (Bool (Set (Var "X"))  ($#r1_pboole :::"in"::: )  (Set   ($#k1_mboolean :::"bool"::: )  (Set (Var "A"))))  ")" ))) ; 
 
theorem :: MBOOLEAN:19 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds"  (Bool (Set   ($#k7_pboole :::"(Funcs)"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r2_pboole :::"c="::: )  (Set   ($#k1_mboolean :::"bool"::: )  (Set  ($#k6_pboole :::"[|"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_pboole :::"|]"::: ) ))))) ; 
 begin  definitionlet "I" be    ($#m1_hidden :::"set"::: )  ; let "A" be   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); func  :::"union"::: "A" ->   ($#m1_hidden :::"ManySortedSet":::) "of" "I" means :: MBOOLEAN:def 2 (Bool  "for" (Set (Var "i")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  "I")) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set  "(" "A"  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" )))); end; 






:: deftheorem    defines :::"union"::: MBOOLEAN:def 2 :  (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "b3")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_mboolean :::"union"::: )  (Set (Var "A")))) "iff" (Bool  "for" (Set (Var "i")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set (Var "I")))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set  "(" (Set (Var "A"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")) ")" ))))  ")" ))); 
 registrationlet "I" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k2_mboolean :::"union"::: )  (Set  "("  ($#k1_pboole :::"[[0]]"::: )  "I" ")" )) -> bbbadV3_RELAT_1() ; 
end; 
theorem :: MBOOLEAN:20 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "X")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds"   (Bool  "("  (Bool (Set (Var "A"))  ($#r1_pboole :::"in"::: )  (Set   ($#k2_mboolean :::"union"::: )  (Set (Var "X")))) "iff" (Bool  "ex" (Set (Var "Y")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_pboole :::"in"::: )  (Set (Var "Y"))) & (Bool (Set (Var "Y"))  ($#r1_pboole :::"in"::: )  (Set (Var "X")))  ")" ))  ")" ))) ; 
 
theorem :: MBOOLEAN:21 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k2_mboolean :::"union"::: )  (Set  "("  ($#k1_pboole :::"[[0]]"::: )  (Set (Var "I")) ")" ))  ($#r6_pboole :::"="::: )  (Set   ($#k1_pboole :::"[[0]]"::: )  (Set (Var "I"))))) ; 
 
theorem :: MBOOLEAN:22 (Bool  "for" (Set (Var "I")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k2_mboolean :::"union"::: )  (Set  "(" (Set (Var "I"))  ($#k7_funcop_1 :::"-->"::: )  (Set (Var "x")) ")" ))  ($#r6_pboole :::"="::: )  (Set (Set (Var "I"))  ($#k7_funcop_1 :::"-->"::: )  (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "x")) ")" )))) ; 
 
theorem :: MBOOLEAN:23 (Bool  "for" (Set (Var "I")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k2_mboolean :::"union"::: )  (Set  "(" (Set (Var "I"))  ($#k7_funcop_1 :::"-->"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ))  ($#r6_pboole :::"="::: )  (Set (Set (Var "I"))  ($#k7_funcop_1 :::"-->"::: )  (Set (Var "x"))))) ; 
 
theorem :: MBOOLEAN:24 (Bool  "for" (Set (Var "I")) "," (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k2_mboolean :::"union"::: )  (Set  "(" (Set (Var "I"))  ($#k7_funcop_1 :::"-->"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) ($#k2_tarski :::"}"::: ) ) ")" ))  ($#r6_pboole :::"="::: )  (Set (Set (Var "I"))  ($#k7_funcop_1 :::"-->"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )))) ; 
 
theorem :: MBOOLEAN:25 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "," (Set (Var "A")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool (Set (Var "X"))  ($#r1_pboole :::"in"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Var "X"))  ($#r2_pboole :::"c="::: )  (Set   ($#k2_mboolean :::"union"::: )  (Set (Var "A")))))) ; 
 
theorem :: MBOOLEAN:26 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool (Set (Var "A"))  ($#r2_pboole :::"c="::: )  (Set (Var "B")))) "holds"  (Bool (Set   ($#k2_mboolean :::"union"::: )  (Set (Var "A")))  ($#r2_pboole :::"c="::: )  (Set   ($#k2_mboolean :::"union"::: )  (Set (Var "B")))))) ; 
 
theorem :: MBOOLEAN:27 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds"  (Bool (Set   ($#k2_mboolean :::"union"::: )  (Set  "(" (Set (Var "A"))  ($#k2_pboole :::"\/"::: )  (Set (Var "B")) ")" ))  ($#r6_pboole :::"="::: )  (Set (Set  "("  ($#k2_mboolean :::"union"::: )  (Set (Var "A")) ")" )  ($#k2_pboole :::"\/"::: )  (Set  "("  ($#k2_mboolean :::"union"::: )  (Set (Var "B")) ")" ))))) ; 
 
theorem :: MBOOLEAN:28 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds"  (Bool (Set   ($#k2_mboolean :::"union"::: )  (Set  "(" (Set (Var "A"))  ($#k3_pboole :::"/\"::: )  (Set (Var "B")) ")" ))  ($#r2_pboole :::"c="::: )  (Set (Set  "("  ($#k2_mboolean :::"union"::: )  (Set (Var "A")) ")" )  ($#k3_pboole :::"/\"::: )  (Set  "("  ($#k2_mboolean :::"union"::: )  (Set (Var "B")) ")" ))))) ; 
 
theorem :: MBOOLEAN:29 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds"  (Bool (Set   ($#k2_mboolean :::"union"::: )  (Set  "("  ($#k1_mboolean :::"bool"::: )  (Set (Var "A")) ")" ))  ($#r6_pboole :::"="::: )  (Set (Var "A"))))) ; 
 
theorem :: MBOOLEAN:30 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds"  (Bool (Set (Var "A"))  ($#r2_pboole :::"c="::: )  (Set   ($#k1_mboolean :::"bool"::: )  (Set  "("  ($#k2_mboolean :::"union"::: )  (Set (Var "A")) ")" ))))) ; 
 
theorem :: MBOOLEAN:31 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Y")) "," (Set (Var "A")) "," (Set (Var "X")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool (Set   ($#k2_mboolean :::"union"::: )  (Set (Var "Y")))  ($#r2_pboole :::"c="::: )  (Set (Var "A"))) & (Bool (Set (Var "X"))  ($#r1_pboole :::"in"::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Var "X"))  ($#r2_pboole :::"c="::: )  (Set (Var "A"))))) ; 
 
theorem :: MBOOLEAN:32 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Z")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "A")) "being" bbbadV2_RELAT_1()  ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool  "("   "for" (Set (Var "X")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool (Set (Var "X"))  ($#r1_pboole :::"in"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Var "X"))  ($#r2_pboole :::"c="::: )  (Set (Var "Z")))  ")" )) "holds"  (Bool (Set   ($#k2_mboolean :::"union"::: )  (Set (Var "A")))  ($#r2_pboole :::"c="::: )  (Set (Var "Z")))))) ; 
 
theorem :: MBOOLEAN:33 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "A")) "being" bbbadV2_RELAT_1()  ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool  "("   "for" (Set (Var "X")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool (Set (Var "X"))  ($#r1_pboole :::"in"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k3_pboole :::"/\"::: )  (Set (Var "B")))  ($#r6_pboole :::"="::: )  (Set   ($#k1_pboole :::"[[0]]"::: )  (Set (Var "I"))))  ")" )) "holds"  (Bool (Set (Set  "("  ($#k2_mboolean :::"union"::: )  (Set (Var "A")) ")" )  ($#k3_pboole :::"/\"::: )  (Set (Var "B")))  ($#r6_pboole :::"="::: )  (Set   ($#k1_pboole :::"[[0]]"::: )  (Set (Var "I"))))))) ; 
 
theorem :: MBOOLEAN:34 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool (Set (Set (Var "A"))  ($#k2_pboole :::"\/"::: )  (Set (Var "B"))) "is" bbbadV2_RELAT_1()) & (Bool  "("   "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool (Set (Var "X"))  ($#r1_hidden :::"<>"::: )  (Set (Var "Y"))) & (Bool (Set (Var "X"))  ($#r1_pboole :::"in"::: )  (Set (Set (Var "A"))  ($#k2_pboole :::"\/"::: )  (Set (Var "B")))) & (Bool (Set (Var "Y"))  ($#r1_pboole :::"in"::: )  (Set (Set (Var "A"))  ($#k2_pboole :::"\/"::: )  (Set (Var "B"))))) "holds"  (Bool (Set (Set (Var "X"))  ($#k3_pboole :::"/\"::: )  (Set (Var "Y")))  ($#r6_pboole :::"="::: )  (Set   ($#k1_pboole :::"[[0]]"::: )  (Set (Var "I"))))  ")" )) "holds"  (Bool (Set   ($#k2_mboolean :::"union"::: )  (Set  "(" (Set (Var "A"))  ($#k3_pboole :::"/\"::: )  (Set (Var "B")) ")" ))  ($#r6_pboole :::"="::: )  (Set (Set  "("  ($#k2_mboolean :::"union"::: )  (Set (Var "A")) ")" )  ($#k3_pboole :::"/\"::: )  (Set  "("  ($#k2_mboolean :::"union"::: )  (Set (Var "B")) ")" ))))) ; 
 
theorem :: MBOOLEAN:35 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "X")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "B")) "being" bbbadV2_RELAT_1()  ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool (Set (Var "X"))  ($#r2_pboole :::"c="::: )  (Set   ($#k2_mboolean :::"union"::: )  (Set  "(" (Set (Var "A"))  ($#k2_pboole :::"\/"::: )  (Set (Var "B")) ")" ))) & (Bool  "("   "for" (Set (Var "Y")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool (Set (Var "Y"))  ($#r1_pboole :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "Y"))  ($#k3_pboole :::"/\"::: )  (Set (Var "X")))  ($#r6_pboole :::"="::: )  (Set   ($#k1_pboole :::"[[0]]"::: )  (Set (Var "I"))))  ")" )) "holds"  (Bool (Set (Var "X"))  ($#r2_pboole :::"c="::: )  (Set   ($#k2_mboolean :::"union"::: )  (Set (Var "A"))))))) ; 
 
theorem :: MBOOLEAN:36 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being" bbbadV2_RELAT_1() bbbadV2_FINSET_1()  ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool  "("   "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool (Set (Var "X"))  ($#r1_pboole :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "Y"))  ($#r1_pboole :::"in"::: )  (Set (Var "A"))) & (Bool (Bool  "not" (Set (Var "X"))  ($#r2_pboole :::"c="::: )  (Set (Var "Y"))))) "holds"  (Bool (Set (Var "Y"))  ($#r2_pboole :::"c="::: )  (Set (Var "X")))  ")" )) "holds"  (Bool (Set   ($#k2_mboolean :::"union"::: )  (Set (Var "A")))  ($#r1_pboole :::"in"::: )  (Set (Var "A"))))) ;