:: ISOMICHI semantic presentation begin registrationlet "D" be ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_tex_1 :::"ADTS"::: ) "D") -> ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ; end; registration cluster ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v2_tdlat_3 :::"anti-discrete"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; theorem :: ISOMICHI:1 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" ) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "B")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" ) ")" ) ")" ))))) ; theorem :: ISOMICHI:2 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" ) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "B")) ")" ) ")" ) ")" ))))) ; begin definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); attr "A" is :::"supercondensed"::: means :: ISOMICHI:def 1 (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) "A" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tops_1 :::"Int"::: ) "A")); attr "A" is :::"subcondensed"::: means :: ISOMICHI:def 2 (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) "A" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) "A")); end; :: deftheorem defines :::"supercondensed"::: ISOMICHI:def 1 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_isomichi :::"supercondensed"::: ) ) "iff" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")))) ")" ))); :: deftheorem defines :::"subcondensed"::: ISOMICHI:def 2 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_isomichi :::"subcondensed"::: ) ) "iff" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")))) ")" ))); registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#v4_pre_topc :::"closed"::: ) -> ($#v1_isomichi :::"supercondensed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; theorem :: ISOMICHI:3 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v1_isomichi :::"supercondensed"::: ) ))) ; theorem :: ISOMICHI:4 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v2_isomichi :::"subcondensed"::: ) ))) ; definitionlet "T" be ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); redefine attr "A" is :::"condensed"::: means :: ISOMICHI:def 3 (Bool "(" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) "A" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) "A")) & (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) "A" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tops_1 :::"Int"::: ) "A")) ")" ); end; :: deftheorem defines :::"condensed"::: ISOMICHI:def 3 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_tops_1 :::"condensed"::: ) ) "iff" (Bool "(" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")))) & (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")))) ")" ) ")" ))); theorem :: ISOMICHI:5 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_tops_1 :::"condensed"::: ) ) "iff" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_isomichi :::"subcondensed"::: ) ) & (Bool (Set (Var "A")) "is" ($#v1_isomichi :::"supercondensed"::: ) ) ")" ) ")" ))) ; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#v4_tops_1 :::"condensed"::: ) -> ($#v1_isomichi :::"supercondensed"::: ) ($#v2_isomichi :::"subcondensed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); cluster ($#v1_isomichi :::"supercondensed"::: ) ($#v2_isomichi :::"subcondensed"::: ) -> ($#v4_tops_1 :::"condensed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#v4_tops_1 :::"condensed"::: ) ($#v1_isomichi :::"supercondensed"::: ) ($#v2_isomichi :::"subcondensed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; theorem :: ISOMICHI:6 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_isomichi :::"supercondensed"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v2_isomichi :::"subcondensed"::: ) ))) ; theorem :: ISOMICHI:7 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v2_isomichi :::"subcondensed"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v1_isomichi :::"supercondensed"::: ) ))) ; theorem :: ISOMICHI:8 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_isomichi :::"supercondensed"::: ) ) "iff" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) ")" ))) ; theorem :: ISOMICHI:9 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_isomichi :::"subcondensed"::: ) ) "iff" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" ))) ")" ))) ; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#v2_isomichi :::"subcondensed"::: ) -> ($#v1_decomp_1 :::"semi-open"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); cluster ($#v1_decomp_1 :::"semi-open"::: ) -> ($#v2_isomichi :::"subcondensed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; theorem :: ISOMICHI:10 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_tops_1 :::"condensed"::: ) ) "iff" (Bool "(" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" ))) ")" ) ")" ))) ; begin notationlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); synonym :::"regular_open"::: "A" for :::"open_condensed"::: ; end; notationlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); synonym :::"regular_closed"::: "A" for :::"closed_condensed"::: ; end; theorem :: ISOMICHI:11 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T"))) "is" ($#v6_tops_1 :::"regular_open"::: ) ) & (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T"))) "is" ($#v5_tops_1 :::"regular_closed"::: ) ) ")" )) ; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster (Set ($#k2_struct_0 :::"[#]"::: ) "T") -> ($#v5_tops_1 :::"regular_closed"::: ) ($#v6_tops_1 :::"regular_open"::: ) ; end; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v5_tops_1 :::"regular_closed"::: ) ($#v6_tops_1 :::"regular_open"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; theorem :: ISOMICHI:12 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_struct_0 :::"{}"::: ) (Set (Var "T")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_struct_0 :::"{}"::: ) (Set (Var "T"))))) ; theorem :: ISOMICHI:13 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v6_tops_1 :::"regular_open"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v5_tops_1 :::"regular_closed"::: ) ))) ; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#v5_tops_1 :::"regular_closed"::: ) ($#v6_tops_1 :::"regular_open"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#v6_tops_1 :::"regular_open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set "A" ($#k3_subset_1 :::"`"::: ) ) -> ($#v5_tops_1 :::"regular_closed"::: ) ; end; theorem :: ISOMICHI:14 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v5_tops_1 :::"regular_closed"::: ) )) "holds" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v6_tops_1 :::"regular_open"::: ) ))) ; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#v5_tops_1 :::"regular_closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set "A" ($#k3_subset_1 :::"`"::: ) ) -> ($#v6_tops_1 :::"regular_open"::: ) ; end; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#v6_tops_1 :::"regular_open"::: ) -> ($#v3_pre_topc :::"open"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); cluster ($#v5_tops_1 :::"regular_closed"::: ) -> ($#v4_pre_topc :::"closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; theorem :: ISOMICHI:15 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" )) "is" ($#v6_tops_1 :::"regular_open"::: ) ) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" )) "is" ($#v5_tops_1 :::"regular_closed"::: ) ) ")" ))) ; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) "A" ")" )) -> ($#v6_tops_1 :::"regular_open"::: ) ; cluster (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) "A" ")" )) -> ($#v5_tops_1 :::"regular_closed"::: ) ; end; theorem :: ISOMICHI:16 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v6_tops_1 :::"regular_open"::: ) ) "iff" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_isomichi :::"supercondensed"::: ) ) & (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) ")" ) ")" ))) ; theorem :: ISOMICHI:17 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v5_tops_1 :::"regular_closed"::: ) ) "iff" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_isomichi :::"subcondensed"::: ) ) & (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ) ")" ) ")" ))) ; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#v6_tops_1 :::"regular_open"::: ) -> ($#v3_pre_topc :::"open"::: ) ($#v4_tops_1 :::"condensed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); cluster ($#v3_pre_topc :::"open"::: ) ($#v4_tops_1 :::"condensed"::: ) -> ($#v6_tops_1 :::"regular_open"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); cluster ($#v5_tops_1 :::"regular_closed"::: ) -> ($#v4_pre_topc :::"closed"::: ) ($#v4_tops_1 :::"condensed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); cluster ($#v4_pre_topc :::"closed"::: ) ($#v4_tops_1 :::"condensed"::: ) -> ($#v5_tops_1 :::"regular_closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; theorem :: ISOMICHI:18 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_tops_1 :::"condensed"::: ) ) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "B")) "is" ($#v6_tops_1 :::"regular_open"::: ) ) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "B")))) ")" )) ")" ))) ; theorem :: ISOMICHI:19 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_tops_1 :::"condensed"::: ) ) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "B")) "is" ($#v5_tops_1 :::"regular_closed"::: ) ) & (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "B"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) ")" )) ")" ))) ; begin definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); redefine func :::"Fr"::: "A" equals :: ISOMICHI:def 4 (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) "A" ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) "A" ")" )); end; :: deftheorem defines :::"Fr"::: ISOMICHI:def 4 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k2_tops_1 :::"Fr"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" ))))); theorem :: ISOMICHI:20 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_tops_1 :::"condensed"::: ) ) "iff" (Bool "(" (Bool (Set ($#k2_tops_1 :::"Fr"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" ) ")" ))) & (Bool (Set ($#k2_tops_1 :::"Fr"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) ")" ))) ")" ) ")" ))) ; definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); func :::"Border"::: "A" -> ($#m1_subset_1 :::"Subset":::) "of" "T" equals :: ISOMICHI:def 5 (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_tops_1 :::"Fr"::: ) "A" ")" )); end; :: deftheorem defines :::"Border"::: ISOMICHI:def 5 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k1_isomichi :::"Border"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_tops_1 :::"Fr"::: ) (Set (Var "A")) ")" ))))); theorem :: ISOMICHI:21 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set ($#k1_isomichi :::"Border"::: ) (Set (Var "A"))) "is" ($#v6_tops_1 :::"regular_open"::: ) ) & (Bool (Set ($#k1_isomichi :::"Border"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" ) ")" ))) & (Bool (Set ($#k1_isomichi :::"Border"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" ) ")" ) ")" ))) ")" ))) ; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set ($#k1_isomichi :::"Border"::: ) "A") -> ($#v6_tops_1 :::"regular_open"::: ) ; end; theorem :: ISOMICHI:22 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_isomichi :::"supercondensed"::: ) ) "iff" (Bool "(" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A"))) "is" ($#v6_tops_1 :::"regular_open"::: ) ) & (Bool (Set ($#k1_isomichi :::"Border"::: ) (Set (Var "A"))) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) ")" ))) ; theorem :: ISOMICHI:23 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_isomichi :::"subcondensed"::: ) ) "iff" (Bool "(" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) "is" ($#v5_tops_1 :::"regular_closed"::: ) ) & (Bool (Set ($#k1_isomichi :::"Border"::: ) (Set (Var "A"))) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) ")" ))) ; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set ($#k1_isomichi :::"Border"::: ) (Set "(" ($#k1_isomichi :::"Border"::: ) "A" ")" )) -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: ISOMICHI:24 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_tops_1 :::"condensed"::: ) ) "iff" (Bool "(" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A"))) "is" ($#v6_tops_1 :::"regular_open"::: ) ) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) "is" ($#v5_tops_1 :::"regular_closed"::: ) ) & (Bool (Set ($#k1_isomichi :::"Border"::: ) (Set (Var "A"))) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ) ")" ))) ; begin theorem :: ISOMICHI:25 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "a")) ($#k4_rcomp_1 :::".]"::: ) ))) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "a")) ($#k2_rcomp_1 :::".["::: ) )))) ; theorem :: ISOMICHI:26 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k3_rcomp_1 :::".["::: ) ))) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k2_rcomp_1 :::".["::: ) )))) ; theorem :: ISOMICHI:27 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "a")) ($#k4_rcomp_1 :::".]"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_borsuk_5 :::"IRRAT"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "b")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k3_rcomp_1 :::".["::: ) )))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k3_topmetr :::"R^1"::: ) ))))) ; theorem :: ISOMICHI:28 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_borsuk_5 :::"RAT"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: ISOMICHI:29 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k3_borsuk_5 :::"IRRAT"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: ISOMICHI:30 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k3_borsuk_5 :::"IRRAT"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: ISOMICHI:31 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k3_borsuk_5 :::"IRRAT"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k3_rcomp_1 :::".["::: ) ))) ; theorem :: ISOMICHI:32 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "a")) ($#k2_rcomp_1 :::".["::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_borsuk_5 :::"RAT"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" ))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "c")))) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "a")) ($#k2_rcomp_1 :::".["::: ) )))) ; theorem :: ISOMICHI:33 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k1_numbers :::"REAL"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "a")) ($#k2_rcomp_1 :::".["::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "b")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k2_rcomp_1 :::".["::: ) )))) ; theorem :: ISOMICHI:34 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "a")) ($#k4_rcomp_1 :::".]"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "b")) "," (Set (Var "c")) ($#k1_rcomp_1 :::".]"::: ) ))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "c")))) "holds" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "a")) ($#k2_rcomp_1 :::".["::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "b")) "," (Set (Var "c")) ($#k2_rcomp_1 :::".["::: ) ))))) ; begin notationlet "A", "B" be ($#m1_hidden :::"set"::: ) ; antonym "A" "," "B" :::"are_c=-incomparable"::: for "A" "," "B" :::"are_c=-comparable"::: ; end; theorem :: ISOMICHI:35 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r3_xboole_0 :::"are_c=-incomparable"::: ) ) "or" (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) "or" (Bool (Set (Var "B")) ($#r2_xboole_0 :::"c<"::: ) (Set (Var "A"))) ")" )) ; definitionlet "T" be ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); attr "A" is :::"1st_class"::: means :: ISOMICHI:def 6 (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) "A" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) "A" ")" ))); attr "A" is :::"2nd_class"::: means :: ISOMICHI:def 7 (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) "A" ")" )) ($#r2_xboole_0 :::"c<"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) "A" ")" ))); attr "A" is :::"3rd_class"::: means :: ISOMICHI:def 8 (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) "A" ")" )) "," (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) "A" ")" )) ($#r3_xboole_0 :::"are_c=-incomparable"::: ) ); end; :: deftheorem defines :::"1st_class"::: ISOMICHI:def 6 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_isomichi :::"1st_class"::: ) ) "iff" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" ))) ")" ))); :: deftheorem defines :::"2nd_class"::: ISOMICHI:def 7 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_isomichi :::"2nd_class"::: ) ) "iff" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" )) ($#r2_xboole_0 :::"c<"::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" ))) ")" ))); :: deftheorem defines :::"3rd_class"::: ISOMICHI:def 8 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v5_isomichi :::"3rd_class"::: ) ) "iff" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" )) "," (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" )) ($#r3_xboole_0 :::"are_c=-incomparable"::: ) ) ")" ))); theorem :: ISOMICHI:36 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_isomichi :::"1st_class"::: ) ) "or" (Bool (Set (Var "A")) "is" ($#v4_isomichi :::"2nd_class"::: ) ) "or" (Bool (Set (Var "A")) "is" ($#v5_isomichi :::"3rd_class"::: ) ) ")" ))) ; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#v3_isomichi :::"1st_class"::: ) -> ($#~v4_isomichi "non" ($#v4_isomichi :::"2nd_class"::: ) ) ($#~v5_isomichi "non" ($#v5_isomichi :::"3rd_class"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); cluster ($#v4_isomichi :::"2nd_class"::: ) -> ($#~v3_isomichi "non" ($#v3_isomichi :::"1st_class"::: ) ) ($#~v5_isomichi "non" ($#v5_isomichi :::"3rd_class"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); cluster ($#v5_isomichi :::"3rd_class"::: ) -> ($#~v3_isomichi "non" ($#v3_isomichi :::"1st_class"::: ) ) ($#~v4_isomichi "non" ($#v4_isomichi :::"2nd_class"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; theorem :: ISOMICHI:37 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_isomichi :::"1st_class"::: ) ) "iff" (Bool (Set ($#k1_isomichi :::"Border"::: ) (Set (Var "A"))) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" ))) ; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#v1_isomichi :::"supercondensed"::: ) -> ($#v3_isomichi :::"1st_class"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); cluster ($#v2_isomichi :::"subcondensed"::: ) -> ($#v3_isomichi :::"1st_class"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; definitionlet "T" be ($#l1_pre_topc :::"TopSpace":::); attr "T" is :::"with_1st_class_subsets"::: means :: ISOMICHI:def 9 (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool (Set (Var "A")) "is" ($#v3_isomichi :::"1st_class"::: ) )); attr "T" is :::"with_2nd_class_subsets"::: means :: ISOMICHI:def 10 (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool (Set (Var "A")) "is" ($#v4_isomichi :::"2nd_class"::: ) )); attr "T" is :::"with_3rd_class_subsets"::: means :: ISOMICHI:def 11 (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool (Set (Var "A")) "is" ($#v5_isomichi :::"3rd_class"::: ) )); end; :: deftheorem defines :::"with_1st_class_subsets"::: ISOMICHI:def 9 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v6_isomichi :::"with_1st_class_subsets"::: ) ) "iff" (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Set (Var "A")) "is" ($#v3_isomichi :::"1st_class"::: ) )) ")" )); :: deftheorem defines :::"with_2nd_class_subsets"::: ISOMICHI:def 10 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v7_isomichi :::"with_2nd_class_subsets"::: ) ) "iff" (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Set (Var "A")) "is" ($#v4_isomichi :::"2nd_class"::: ) )) ")" )); :: deftheorem defines :::"with_3rd_class_subsets"::: ISOMICHI:def 11 : (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v8_isomichi :::"with_3rd_class_subsets"::: ) ) "iff" (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Set (Var "A")) "is" ($#v5_isomichi :::"3rd_class"::: ) )) ")" )); registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_tdlat_3 :::"anti-discrete"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_subset_1 :::"proper"::: ) -> ($#v4_isomichi :::"2nd_class"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; registrationlet "T" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_tdlat_3 :::"anti-discrete"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#v4_isomichi :::"2nd_class"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; registration cluster ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v6_isomichi :::"with_1st_class_subsets"::: ) ($#v7_isomichi :::"with_2nd_class_subsets"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v8_isomichi :::"with_3rd_class_subsets"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#v3_isomichi :::"1st_class"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; registrationlet "T" be ($#v7_isomichi :::"with_2nd_class_subsets"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#v4_isomichi :::"2nd_class"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; registrationlet "T" be ($#v8_isomichi :::"with_3rd_class_subsets"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster ($#v5_isomichi :::"3rd_class"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; theorem :: ISOMICHI:38 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_isomichi :::"1st_class"::: ) ) "iff" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v3_isomichi :::"1st_class"::: ) ) ")" ))) ; theorem :: ISOMICHI:39 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_isomichi :::"2nd_class"::: ) ) "iff" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v4_isomichi :::"2nd_class"::: ) ) ")" ))) ; theorem :: ISOMICHI:40 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v5_isomichi :::"3rd_class"::: ) ) "iff" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) "is" ($#v5_isomichi :::"3rd_class"::: ) ) ")" ))) ; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#v3_isomichi :::"1st_class"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set "A" ($#k3_subset_1 :::"`"::: ) ) -> ($#v3_isomichi :::"1st_class"::: ) ; end; registrationlet "T" be ($#v7_isomichi :::"with_2nd_class_subsets"::: ) ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#v4_isomichi :::"2nd_class"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set "A" ($#k3_subset_1 :::"`"::: ) ) -> ($#v4_isomichi :::"2nd_class"::: ) ; end; registrationlet "T" be ($#v8_isomichi :::"with_3rd_class_subsets"::: ) ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#v5_isomichi :::"3rd_class"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set "A" ($#k3_subset_1 :::"`"::: ) ) -> ($#v5_isomichi :::"3rd_class"::: ) ; end; theorem :: ISOMICHI:41 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_isomichi :::"1st_class"::: ) )) "holds" (Bool "(" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" ) ")" ))) & (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" ) ")" ))) ")" ))) ; theorem :: ISOMICHI:42 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool "(" (Bool (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" ) ")" ))) "or" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" ) ")" ))) ")" )) "holds" (Bool (Set (Var "A")) "is" ($#v3_isomichi :::"1st_class"::: ) ))) ; theorem :: ISOMICHI:43 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_isomichi :::"1st_class"::: ) ) & (Bool (Set (Var "B")) "is" ($#v3_isomichi :::"1st_class"::: ) )) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set (Var "B")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tops_1 :::"Int"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B")) ")" ) ")" ))) & (Bool (Set (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "A")) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set (Var "B")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set "(" ($#k1_tops_1 :::"Int"::: ) (Set "(" (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B")) ")" ) ")" ))) ")" ))) ; theorem :: ISOMICHI:44 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_isomichi :::"1st_class"::: ) ) & (Bool (Set (Var "B")) "is" ($#v3_isomichi :::"1st_class"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "A")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "B"))) "is" ($#v3_isomichi :::"1st_class"::: ) ) & (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "B"))) "is" ($#v3_isomichi :::"1st_class"::: ) ) ")" ))) ;