:: ZF_COLLA  semantic presentation begin  

































definitionlet "E" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "A" be   ($#m1_hidden :::"Ordinal":::); func  :::"Collapse":::  "(" "E" "," "A" ")"  ->    ($#m1_hidden :::"set"::: )   means :: ZF_COLLA:def 1 (Bool  "ex" (Set (Var "L")) "being"   ($#m1_hidden :::"T-Sequence":::) "st"  (Bool  "("  (Bool it  ($#r1_hidden :::"="::: )   "{"  (Set (Var "d")) where d "is"    ($#m1_subset_1 :::"Element"::: )   "of" "E" : (Bool  "for" (Set (Var "d1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" "E"  "st" (Bool (Bool (Set (Var "d1"))  ($#r2_hidden :::"in"::: )  (Set (Var "d")))) "holds"  (Bool  "ex" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::) "st"  (Bool  "("  (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "L")))) & (Bool (Set (Var "d1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"union"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "(" (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "B")) ")" ) ($#k1_tarski :::"}"::: ) )))  ")" )))  "}"  ) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  "A") & (Bool  "("   "for" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  "A")) "holds"  (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "d1")) where d1 "is"    ($#m1_subset_1 :::"Element"::: )   "of" "E" : (Bool  "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" "E"  "st" (Bool (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set (Var "d1")))) "holds"  (Bool  "ex" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::) "st"  (Bool  "("  (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "L"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "B")) ")" ))) & (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"union"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "(" (Set  "(" (Set (Var "L"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "B")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "C")) ")" ) ($#k1_tarski :::"}"::: ) )))  ")" )))  "}"  )  ")" )  ")" )); end; 






:: deftheorem    defines :::"Collapse"::: ZF_COLLA:def 1 :  (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "b3")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_zf_colla :::"Collapse"::: )   "(" (Set (Var "E")) "," (Set (Var "A")) ")" )) "iff" (Bool  "ex" (Set (Var "L")) "being"   ($#m1_hidden :::"T-Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "d")) where d "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "E")) : (Bool  "for" (Set (Var "d1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "E"))  "st" (Bool (Bool (Set (Var "d1"))  ($#r2_hidden :::"in"::: )  (Set (Var "d")))) "holds"  (Bool  "ex" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::) "st"  (Bool  "("  (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "L")))) & (Bool (Set (Var "d1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"union"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "(" (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "B")) ")" ) ($#k1_tarski :::"}"::: ) )))  ")" )))  "}"  ) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set (Var "A"))) & (Bool  "("   "for" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "d1")) where d1 "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "E")) : (Bool  "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "E"))  "st" (Bool (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set (Var "d1")))) "holds"  (Bool  "ex" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::) "st"  (Bool  "("  (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "L"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "B")) ")" ))) & (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_tarski :::"union"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "(" (Set  "(" (Set (Var "L"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "B")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "C")) ")" ) ($#k1_tarski :::"}"::: ) )))  ")" )))  "}"  )  ")" )  ")" ))  ")" )))); 
 
theorem :: ZF_COLLA:1 (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set   ($#k1_zf_colla :::"Collapse"::: )   "(" (Set (Var "E")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "d")) where d "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "E")) : (Bool  "for" (Set (Var "d1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "E"))  "st" (Bool (Bool (Set (Var "d1"))  ($#r2_hidden :::"in"::: )  (Set (Var "d")))) "holds"  (Bool  "ex" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::) "st"  (Bool  "("  (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "d1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_zf_colla :::"Collapse"::: )   "(" (Set (Var "E")) "," (Set (Var "B")) ")" ))  ")" )))  "}"  ))) ; 
 
theorem :: ZF_COLLA:2 (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "E")) "holds"   (Bool  "("  (Bool  "("   "for" (Set (Var "d1")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "E"))  "holds" (Bool (Bool  "not" (Set (Var "d1"))  ($#r2_hidden :::"in"::: )  (Set (Var "d"))))  ")" ) "iff" (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_zf_colla :::"Collapse"::: )   "(" (Set (Var "E")) "," (Set  ($#k1_xboole_0 :::"{}"::: ) ) ")" ))  ")" ))) ; 
 
theorem :: ZF_COLLA:3 (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "E")) "holds"   (Bool  "("  (Bool (Set (Set (Var "d"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "E")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_zf_colla :::"Collapse"::: )   "(" (Set (Var "E")) "," (Set (Var "A")) ")" )) "iff" (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_zf_colla :::"Collapse"::: )   "(" (Set (Var "E")) "," (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")) ")" ) ")" ))  ")" )))) ; 
 
theorem :: ZF_COLLA:4 (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "B")))) "holds"  (Bool (Set   ($#k1_zf_colla :::"Collapse"::: )   "(" (Set (Var "E")) "," (Set (Var "A")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_zf_colla :::"Collapse"::: )   "(" (Set (Var "E")) "," (Set (Var "B")) ")" )))) ; 
 
theorem :: ZF_COLLA:5 (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "E")) (Bool  "ex" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "st" (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_zf_colla :::"Collapse"::: )   "(" (Set (Var "E")) "," (Set (Var "A")) ")" ))))) ; 
 
theorem :: ZF_COLLA:6 (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "d9")) "," (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "E"))  "st" (Bool (Bool (Set (Var "d9"))  ($#r2_hidden :::"in"::: )  (Set (Var "d"))) & (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_zf_colla :::"Collapse"::: )   "(" (Set (Var "E")) "," (Set (Var "A")) ")" ))) "holds"  (Bool  "("  (Bool (Set (Var "d9"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_zf_colla :::"Collapse"::: )   "(" (Set (Var "E")) "," (Set (Var "A")) ")" )) & (Bool  "ex" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::) "st"  (Bool  "("  (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "d9"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_zf_colla :::"Collapse"::: )   "(" (Set (Var "E")) "," (Set (Var "B")) ")" ))  ")" ))  ")" )))) ; 
 
theorem :: ZF_COLLA:7 (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set   ($#k1_zf_colla :::"Collapse"::: )   "(" (Set (Var "E")) "," (Set (Var "A")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "E"))))) ; 
 
theorem :: ZF_COLLA:8 (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "st" (Bool (Set (Var "E"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_zf_colla :::"Collapse"::: )   "(" (Set (Var "E")) "," (Set (Var "A")) ")" )))) ; 
 
theorem :: ZF_COLLA:9 (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "st"  (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "E"))) & (Bool  "("   "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "E")) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "d")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k7_relat_1 :::".:"::: )  (Set (Var "d"))))  ")" )  ")" ))) ; 
 definitionlet "f" be   ($#m1_hidden :::"Function":::); let "X", "Y" be    ($#m1_hidden :::"set"::: )  ; pred "f" :::"is_epsilon-isomorphism_of"::: "X" "," "Y" means :: ZF_COLLA:def 2 (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  "f")  ($#r1_hidden :::"="::: )  "X") & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  "f")  ($#r1_hidden :::"="::: )  "Y") & (Bool "f" "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (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  "("  (Bool  "ex" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "Z"))  ($#r1_hidden :::"="::: )  (Set (Var "y"))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))  ")" )) "iff" (Bool  "ex" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set "f"  ($#k1_funct_1 :::"."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Var "Z"))) & (Bool (Set "f"  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))  ")" ))  ")" )  ")" )  ")" ); end; 






:: deftheorem    defines :::"is_epsilon-isomorphism_of"::: ZF_COLLA:def 2 :  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r1_zf_colla :::"is_epsilon-isomorphism_of"::: )  (Set (Var "X")) "," (Set (Var "Y"))) "iff" (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "Y"))) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (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  "("  (Bool  "ex" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "Z"))  ($#r1_hidden :::"="::: )  (Set (Var "y"))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))  ")" )) "iff" (Bool  "ex" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Var "Z"))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))  ")" ))  ")" )  ")" )  ")" )  ")" ))); 
 definitionlet "X", "Y" be    ($#m1_hidden :::"set"::: )  ; pred "X" "," "Y" :::"are_epsilon-isomorphic":::  means :: ZF_COLLA:def 3 (Bool  "ex" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "st" (Bool (Set (Var "f"))  ($#r1_zf_colla :::"is_epsilon-isomorphism_of"::: )  "X" "," "Y")); end; 





:: deftheorem    defines :::"are_epsilon-isomorphic"::: ZF_COLLA:def 3 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X")) "," (Set (Var "Y"))  ($#r2_zf_colla :::"are_epsilon-isomorphic"::: )  ) "iff" (Bool  "ex" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "st" (Bool (Set (Var "f"))  ($#r1_zf_colla :::"is_epsilon-isomorphism_of"::: )  (Set (Var "X")) "," (Set (Var "Y"))))  ")" )); 
 
theorem :: ZF_COLLA:10 (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "E"))) & (Bool  "("   "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "E")) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "d")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k7_relat_1 :::".:"::: )  (Set (Var "d"))))  ")" )) "holds"  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f"))) "is"   ($#v1_ordinal1 :::"epsilon-transitive"::: )  ))) ; 
 


















theorem :: ZF_COLLA:11 (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "E"))  ($#r2_zf_model :::"|="::: )  (Set   ($#k6_zf_model :::"the_axiom_of_extensionality"::: )  ))) "holds"  (Bool  "for" (Set (Var "u")) "," (Set (Var "v")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "E"))  "st" (Bool (Bool  "("   "for" (Set (Var "w")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "E")) "holds"   (Bool  "("  (Bool (Set (Var "w"))  ($#r2_hidden :::"in"::: )  (Set (Var "u"))) "iff" (Bool (Set (Var "w"))  ($#r2_hidden :::"in"::: )  (Set (Var "v")))  ")" )  ")" )) "holds"  (Bool (Set (Var "u"))  ($#r1_hidden :::"="::: )  (Set (Var "v"))))) ; 
 
theorem :: ZF_COLLA:12 (Bool  "for" (Set (Var "E")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "E"))  ($#r2_zf_model :::"|="::: )  (Set   ($#k6_zf_model :::"the_axiom_of_extensionality"::: )  ))) "holds"  (Bool  "ex" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v1_ordinal1 :::"epsilon-transitive"::: )  ) & (Bool (Set (Var "E")) "," (Set (Var "X"))  ($#r2_zf_colla :::"are_epsilon-isomorphic"::: )  )  ")" ))) ;