:: ISOMICHI semantic presentation begin registration let D be non trivial set ; cluster ADTS D -> non trivial ; coherence not ADTS D is trivial proof ADTS D = TopStruct(# D,(cobool D) #) by TEX_1:def_3; hence not ADTS D is trivial ; ::_thesis: verum end; end; registration cluster non trivial strict TopSpace-like anti-discrete for TopStruct ; existence ex b1 being TopSpace st ( b1 is anti-discrete & not b1 is trivial & b1 is strict ) proof set D = the non trivial set ; take ADTS the non trivial set ; ::_thesis: ( ADTS the non trivial set is anti-discrete & not ADTS the non trivial set is trivial & ADTS the non trivial set is strict ) thus ( ADTS the non trivial set is anti-discrete & not ADTS the non trivial set is trivial & ADTS the non trivial set is strict ) ; ::_thesis: verum end; end; theorem Th1: :: ISOMICHI:1 for T being TopSpace for A, B being Subset of T holds (Int (Cl (Int A))) /\ (Int (Cl (Int B))) = Int (Cl (Int (A /\ B))) proof let T be TopSpace; ::_thesis: for A, B being Subset of T holds (Int (Cl (Int A))) /\ (Int (Cl (Int B))) = Int (Cl (Int (A /\ B))) let A, B be Subset of T; ::_thesis: (Int (Cl (Int A))) /\ (Int (Cl (Int B))) = Int (Cl (Int (A /\ B))) set C = Int A; set D = Int B; (Int (Cl (Int A))) /\ (Int (Cl (Int B))) = Int (Cl ((Int A) /\ (Int B))) by TDLAT_1:7; hence (Int (Cl (Int A))) /\ (Int (Cl (Int B))) = Int (Cl (Int (A /\ B))) by TOPS_1:17; ::_thesis: verum end; theorem Th2: :: ISOMICHI:2 for T being TopSpace for A, B being Subset of T holds Cl (Int (Cl (A \/ B))) = (Cl (Int (Cl A))) \/ (Cl (Int (Cl B))) proof let T be TopSpace; ::_thesis: for A, B being Subset of T holds Cl (Int (Cl (A \/ B))) = (Cl (Int (Cl A))) \/ (Cl (Int (Cl B))) let A, B be Subset of T; ::_thesis: Cl (Int (Cl (A \/ B))) = (Cl (Int (Cl A))) \/ (Cl (Int (Cl B))) set C = Cl A; set D = Cl B; (Cl (Int (Cl A))) \/ (Cl (Int (Cl B))) = Cl (Int ((Cl A) \/ (Cl B))) by TDLAT_1:6; hence Cl (Int (Cl (A \/ B))) = (Cl (Int (Cl A))) \/ (Cl (Int (Cl B))) by PRE_TOPC:20; ::_thesis: verum end; begin definition let T be TopStruct ; let A be Subset of T; attrA is supercondensed means :Def1: :: ISOMICHI:def 1 Int (Cl A) = Int A; attrA is subcondensed means :Def2: :: ISOMICHI:def 2 Cl (Int A) = Cl A; end; :: deftheorem Def1 defines supercondensed ISOMICHI:def_1_:_ for T being TopStruct for A being Subset of T holds ( A is supercondensed iff Int (Cl A) = Int A ); :: deftheorem Def2 defines subcondensed ISOMICHI:def_2_:_ for T being TopStruct for A being Subset of T holds ( A is subcondensed iff Cl (Int A) = Cl A ); registration let T be TopSpace; cluster closed -> supercondensed for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is closed holds b1 is supercondensed proof let A be Subset of T; ::_thesis: ( A is closed implies A is supercondensed ) assume A is closed ; ::_thesis: A is supercondensed then Int (Cl A) = Int A by PRE_TOPC:22; hence A is supercondensed by Def1; ::_thesis: verum end; end; theorem :: ISOMICHI:3 for T being TopSpace for A being Subset of T st A is closed holds A is supercondensed ; theorem Th4: :: ISOMICHI:4 for T being TopSpace for A being Subset of T st A is open holds A is subcondensed proof let T be TopSpace; ::_thesis: for A being Subset of T st A is open holds A is subcondensed let A be Subset of T; ::_thesis: ( A is open implies A is subcondensed ) assume A is open ; ::_thesis: A is subcondensed then Cl (Int A) = Cl A by TOPS_1:23; hence A is subcondensed by Def2; ::_thesis: verum end; definition let T be TopSpace; let A be Subset of T; redefine attr A is condensed means :Def3: :: ISOMICHI:def 3 ( Cl (Int A) = Cl A & Int (Cl A) = Int A ); compatibility ( A is condensed iff ( Cl (Int A) = Cl A & Int (Cl A) = Int A ) ) proof thus ( A is condensed implies ( Cl (Int A) = Cl A & Int (Cl A) = Int A ) ) by TDLAT_3:9; ::_thesis: ( Cl (Int A) = Cl A & Int (Cl A) = Int A implies A is condensed ) assume that A1: Cl (Int A) = Cl A and A2: Int (Cl A) = Int A ; ::_thesis: A is condensed A3: Int A c= A by TOPS_1:16; A c= Cl (Int A) by A1, PRE_TOPC:18; hence A is condensed by A2, A3, TOPS_1:def_6; ::_thesis: verum end; end; :: deftheorem Def3 defines condensed ISOMICHI:def_3_:_ for T being TopSpace for A being Subset of T holds ( A is condensed iff ( Cl (Int A) = Cl A & Int (Cl A) = Int A ) ); theorem Th5: :: ISOMICHI:5 for T being TopSpace for A being Subset of T holds ( A is condensed iff ( A is subcondensed & A is supercondensed ) ) proof let T be TopSpace; ::_thesis: for A being Subset of T holds ( A is condensed iff ( A is subcondensed & A is supercondensed ) ) let A be Subset of T; ::_thesis: ( A is condensed iff ( A is subcondensed & A is supercondensed ) ) thus ( A is condensed implies ( A is subcondensed & A is supercondensed ) ) ::_thesis: ( A is subcondensed & A is supercondensed implies A is condensed ) proof assume A1: A is condensed ; ::_thesis: ( A is subcondensed & A is supercondensed ) then A2: Int (Cl A) = Int A by Def3; Cl (Int A) = Cl A by A1, Def3; hence ( A is subcondensed & A is supercondensed ) by A2, Def1, Def2; ::_thesis: verum end; assume that A3: A is subcondensed and A4: A is supercondensed ; ::_thesis: A is condensed A5: Cl (Int A) = Cl A by A3, Def2; Int (Cl A) = Int A by A4, Def1; hence A is condensed by A5, Def3; ::_thesis: verum end; registration let T be TopSpace; cluster condensed -> supercondensed subcondensed for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is condensed holds ( b1 is subcondensed & b1 is supercondensed ) by Th5; cluster supercondensed subcondensed -> condensed for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is subcondensed & b1 is supercondensed holds b1 is condensed by Th5; end; registration let T be TopSpace; cluster condensed supercondensed subcondensed for Element of bool the carrier of T; existence ex b1 being Subset of T st ( b1 is condensed & b1 is subcondensed & b1 is supercondensed ) proof set A = {} T; take {} T ; ::_thesis: ( {} T is condensed & {} T is subcondensed & {} T is supercondensed ) ( {} T is supercondensed & {} T is subcondensed ) by Th4; hence ( {} T is condensed & {} T is subcondensed & {} T is supercondensed ) ; ::_thesis: verum end; end; theorem :: ISOMICHI:6 for T being TopSpace for A being Subset of T st A is supercondensed holds A ` is subcondensed proof let T be TopSpace; ::_thesis: for A being Subset of T st A is supercondensed holds A ` is subcondensed let A be Subset of T; ::_thesis: ( A is supercondensed implies A ` is subcondensed ) A1: (Int A) ` = Cl (A `) by TDLAT_3:2; assume A is supercondensed ; ::_thesis: A ` is subcondensed then A2: (Int (Cl A)) ` = (Int A) ` by Def1; (Int (Cl A)) ` = Cl ((Cl A) `) by TDLAT_3:2 .= Cl (Int (A `)) by TDLAT_3:3 ; hence A ` is subcondensed by A2, A1, Def2; ::_thesis: verum end; theorem :: ISOMICHI:7 for T being TopSpace for A being Subset of T st A is subcondensed holds A ` is supercondensed proof let T be TopSpace; ::_thesis: for A being Subset of T st A is subcondensed holds A ` is supercondensed let A be Subset of T; ::_thesis: ( A is subcondensed implies A ` is supercondensed ) A1: (Cl A) ` = Int (A `) by TDLAT_3:3; assume A is subcondensed ; ::_thesis: A ` is supercondensed then A2: (Cl (Int A)) ` = (Cl A) ` by Def2; (Cl (Int A)) ` = Int ((Int A) `) by TDLAT_3:3 .= Int (Cl (A `)) by TDLAT_3:2 ; hence A ` is supercondensed by A2, A1, Def1; ::_thesis: verum end; theorem Th8: :: ISOMICHI:8 for T being TopSpace for A being Subset of T holds ( A is supercondensed iff Int (Cl A) c= A ) proof let T be TopSpace; ::_thesis: for A being Subset of T holds ( A is supercondensed iff Int (Cl A) c= A ) let A be Subset of T; ::_thesis: ( A is supercondensed iff Int (Cl A) c= A ) thus ( A is supercondensed implies Int (Cl A) c= A ) ::_thesis: ( Int (Cl A) c= A implies A is supercondensed ) proof assume A is supercondensed ; ::_thesis: Int (Cl A) c= A then Int (Cl A) = Int A by Def1; hence Int (Cl A) c= A by TOPS_1:16; ::_thesis: verum end; assume Int (Cl A) c= A ; ::_thesis: A is supercondensed then A1: Int (Int (Cl A)) c= Int A by TOPS_1:19; Int A c= Int (Cl A) by PRE_TOPC:18, TOPS_1:19; then Int A = Int (Cl A) by A1, XBOOLE_0:def_10; hence A is supercondensed by Def1; ::_thesis: verum end; theorem Th9: :: ISOMICHI:9 for T being TopSpace for A being Subset of T holds ( A is subcondensed iff A c= Cl (Int A) ) proof let T be TopSpace; ::_thesis: for A being Subset of T holds ( A is subcondensed iff A c= Cl (Int A) ) let A be Subset of T; ::_thesis: ( A is subcondensed iff A c= Cl (Int A) ) thus ( A is subcondensed implies A c= Cl (Int A) ) ::_thesis: ( A c= Cl (Int A) implies A is subcondensed ) proof assume A is subcondensed ; ::_thesis: A c= Cl (Int A) then Cl (Int A) = Cl A by Def2; hence A c= Cl (Int A) by PRE_TOPC:18; ::_thesis: verum end; assume A c= Cl (Int A) ; ::_thesis: A is subcondensed then A1: Cl A c= Cl (Cl (Int A)) by PRE_TOPC:19; Cl (Int A) c= Cl A by PRE_TOPC:19, TOPS_1:16; then Cl (Int A) = Cl A by A1, XBOOLE_0:def_10; hence A is subcondensed by Def2; ::_thesis: verum end; registration let T be TopSpace; cluster subcondensed -> semi-open for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is subcondensed holds b1 is semi-open proof let A be Subset of T; ::_thesis: ( A is subcondensed implies A is semi-open ) assume A is subcondensed ; ::_thesis: A is semi-open then A c= Cl (Int A) by Th9; hence A is semi-open by DECOMP_1:def_2; ::_thesis: verum end; cluster semi-open -> subcondensed for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is semi-open holds b1 is subcondensed proof let A be Subset of T; ::_thesis: ( A is semi-open implies A is subcondensed ) assume A is semi-open ; ::_thesis: A is subcondensed then A c= Cl (Int A) by DECOMP_1:def_2; hence A is subcondensed by Th9; ::_thesis: verum end; end; theorem Th10: :: ISOMICHI:10 for T being TopSpace for A being Subset of T holds ( A is condensed iff ( Int (Cl A) c= A & A c= Cl (Int A) ) ) proof let T be TopSpace; ::_thesis: for A being Subset of T holds ( A is condensed iff ( Int (Cl A) c= A & A c= Cl (Int A) ) ) let A be Subset of T; ::_thesis: ( A is condensed iff ( Int (Cl A) c= A & A c= Cl (Int A) ) ) thus ( A is condensed implies ( Int (Cl A) c= A & A c= Cl (Int A) ) ) by Th8, Th9; ::_thesis: ( Int (Cl A) c= A & A c= Cl (Int A) implies A is condensed ) assume that A1: Int (Cl A) c= A and A2: A c= Cl (Int A) ; ::_thesis: A is condensed A3: A is subcondensed by A2, Th9; A is supercondensed by A1, Th8; hence A is condensed by A3; ::_thesis: verum end; begin notation let T be TopStruct ; let A be Subset of T; synonym regular_open A for open_condensed ; end; notation let T be TopStruct ; let A be Subset of T; synonym regular_closed A for closed_condensed ; end; theorem :: ISOMICHI:11 for T being TopSpace holds ( [#] T is regular_open & [#] T is regular_closed ) proof let T be TopSpace; ::_thesis: ( [#] T is regular_open & [#] T is regular_closed ) A1: Int ([#] T) = [#] T by TOPS_1:15; Cl ([#] T) = [#] T by TOPS_1:2; hence ( [#] T is regular_open & [#] T is regular_closed ) by A1, TOPS_1:def_7, TOPS_1:def_8; ::_thesis: verum end; registration let T be TopSpace; cluster [#] T -> regular_closed regular_open ; coherence ( [#] T is regular_open & [#] T is regular_closed ) proof A1: Int ([#] T) = [#] T by TOPS_1:15; Cl ([#] T) = [#] T by TOPS_1:2; hence ( [#] T is regular_open & [#] T is regular_closed ) by A1, TOPS_1:def_7, TOPS_1:def_8; ::_thesis: verum end; end; registration let T be TopSpace; cluster empty -> regular_closed regular_open for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is empty holds ( b1 is regular_open & b1 is regular_closed ) proof let S be Subset of T; ::_thesis: ( S is empty implies ( S is regular_open & S is regular_closed ) ) assume A1: S is empty ; ::_thesis: ( S is regular_open & S is regular_closed ) then A2: S = Int S ; S = Cl S by A1, PCOMPS_1:2; hence ( S is regular_open & S is regular_closed ) by A2, TOPS_1:def_7, TOPS_1:def_8; ::_thesis: verum end; end; theorem :: ISOMICHI:12 for T being TopSpace holds Int (Cl ({} T)) = {} T proof let T be TopSpace; ::_thesis: Int (Cl ({} T)) = {} T Int (Cl ({} T)) = Int ({} T) by PCOMPS_1:2 .= {} T ; hence Int (Cl ({} T)) = {} T ; ::_thesis: verum end; theorem Th13: :: ISOMICHI:13 for T being TopSpace for A being Subset of T st A is regular_open holds A ` is regular_closed proof let T be TopSpace; ::_thesis: for A being Subset of T st A is regular_open holds A ` is regular_closed let A be Subset of T; ::_thesis: ( A is regular_open implies A ` is regular_closed ) assume A is regular_open ; ::_thesis: A ` is regular_closed then Int (Cl A) = A by TOPS_1:def_8; then Cl ((Cl A) `) = A ` by TDLAT_3:2; then Cl (Int (A `)) = A ` by TDLAT_3:3; hence A ` is regular_closed by TOPS_1:def_7; ::_thesis: verum end; registration let T be TopSpace; cluster regular_closed regular_open for Element of bool the carrier of T; existence ex b1 being Subset of T st ( b1 is regular_open & b1 is regular_closed ) proof take {} T ; ::_thesis: ( {} T is regular_open & {} T is regular_closed ) thus ( {} T is regular_open & {} T is regular_closed ) ; ::_thesis: verum end; end; registration let T be TopSpace; let A be regular_open Subset of T; clusterA ` -> regular_closed ; coherence A ` is regular_closed by Th13; end; theorem Th14: :: ISOMICHI:14 for T being TopSpace for A being Subset of T st A is regular_closed holds A ` is regular_open proof let T be TopSpace; ::_thesis: for A being Subset of T st A is regular_closed holds A ` is regular_open let A be Subset of T; ::_thesis: ( A is regular_closed implies A ` is regular_open ) assume A is regular_closed ; ::_thesis: A ` is regular_open then Cl (Int A) = A by TOPS_1:def_7; then Int ((Int A) `) = A ` by TDLAT_3:3; then Int (Cl (A `)) = A ` by TDLAT_3:2; hence A ` is regular_open by TOPS_1:def_8; ::_thesis: verum end; registration let T be TopSpace; let A be regular_closed Subset of T; clusterA ` -> regular_open ; coherence A ` is regular_open by Th14; end; registration let T be TopSpace; cluster regular_open -> open for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is regular_open holds b1 is open by TOPS_1:67; cluster regular_closed -> closed for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is regular_closed holds b1 is closed by TOPS_1:66; end; theorem Th15: :: ISOMICHI:15 for T being TopSpace for A being Subset of T holds ( Int (Cl A) is regular_open & Cl (Int A) is regular_closed ) proof let T be TopSpace; ::_thesis: for A being Subset of T holds ( Int (Cl A) is regular_open & Cl (Int A) is regular_closed ) let A be Subset of T; ::_thesis: ( Int (Cl A) is regular_open & Cl (Int A) is regular_closed ) A1: Cl (Int (Cl (Int A))) = Cl (Int A) by TOPS_1:26; Int (Cl (Int (Cl A))) = Int (Cl A) by TDLAT_1:5; hence ( Int (Cl A) is regular_open & Cl (Int A) is regular_closed ) by A1, TOPS_1:def_7, TOPS_1:def_8; ::_thesis: verum end; registration let T be TopSpace; let A be Subset of T; cluster Int (Cl A) -> regular_open ; coherence Int (Cl A) is regular_open by Th15; cluster Cl (Int A) -> regular_closed ; coherence Cl (Int A) is regular_closed by Th15; end; theorem :: ISOMICHI:16 for T being TopSpace for A being Subset of T holds ( A is regular_open iff ( A is supercondensed & A is open ) ) proof let T be TopSpace; ::_thesis: for A being Subset of T holds ( A is regular_open iff ( A is supercondensed & A is open ) ) let A be Subset of T; ::_thesis: ( A is regular_open iff ( A is supercondensed & A is open ) ) thus ( A is regular_open implies ( A is supercondensed & A is open ) ) ::_thesis: ( A is supercondensed & A is open implies A is regular_open ) proof assume A is regular_open ; ::_thesis: ( A is supercondensed & A is open ) then A1: Int (Cl A) = A by TOPS_1:def_8; then Int A = A ; hence ( A is supercondensed & A is open ) by A1, Def1; ::_thesis: verum end; assume that A2: A is supercondensed and A3: A is open ; ::_thesis: A is regular_open Int (Cl A) = Int A by A2, Def1; hence A is regular_open by A3, TOPS_1:23; ::_thesis: verum end; theorem :: ISOMICHI:17 for T being TopSpace for A being Subset of T holds ( A is regular_closed iff ( A is subcondensed & A is closed ) ) proof let T be TopSpace; ::_thesis: for A being Subset of T holds ( A is regular_closed iff ( A is subcondensed & A is closed ) ) let A be Subset of T; ::_thesis: ( A is regular_closed iff ( A is subcondensed & A is closed ) ) thus ( A is regular_closed implies ( A is subcondensed & A is closed ) ) ::_thesis: ( A is subcondensed & A is closed implies A is regular_closed ) proof assume A is regular_closed ; ::_thesis: ( A is subcondensed & A is closed ) then A1: Cl (Int A) = A by TOPS_1:def_7; then Cl A = A ; hence ( A is subcondensed & A is closed ) by A1, Def2; ::_thesis: verum end; assume that A2: A is subcondensed and A3: A is closed ; ::_thesis: A is regular_closed Cl (Int A) = Cl A by A2, Def2; hence A is regular_closed by A3, PRE_TOPC:22; ::_thesis: verum end; registration let T be TopSpace; cluster regular_open -> open condensed for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is regular_open holds ( b1 is condensed & b1 is open ) by TOPS_1:67; cluster open condensed -> regular_open for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is condensed & b1 is open holds b1 is regular_open by TOPS_1:67; cluster regular_closed -> closed condensed for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is regular_closed holds ( b1 is condensed & b1 is closed ) by TOPS_1:66; cluster closed condensed -> regular_closed for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is condensed & b1 is closed holds b1 is regular_closed by TOPS_1:66; end; theorem :: ISOMICHI:18 for T being TopSpace for A being Subset of T holds ( A is condensed iff ex B being Subset of T st ( B is regular_open & B c= A & A c= Cl B ) ) proof let T be TopSpace; ::_thesis: for A being Subset of T holds ( A is condensed iff ex B being Subset of T st ( B is regular_open & B c= A & A c= Cl B ) ) let A be Subset of T; ::_thesis: ( A is condensed iff ex B being Subset of T st ( B is regular_open & B c= A & A c= Cl B ) ) thus ( A is condensed implies ex B being Subset of T st ( B is regular_open & B c= A & A c= Cl B ) ) ::_thesis: ( ex B being Subset of T st ( B is regular_open & B c= A & A c= Cl B ) implies A is condensed ) proof assume A1: A is condensed ; ::_thesis: ex B being Subset of T st ( B is regular_open & B c= A & A c= Cl B ) then A2: Cl (Int A) = Cl A by Def3; take Int (Cl A) ; ::_thesis: ( Int (Cl A) is regular_open & Int (Cl A) c= A & A c= Cl (Int (Cl A)) ) Int (Cl A) = Int A by A1, Def3; hence ( Int (Cl A) is regular_open & Int (Cl A) c= A & A c= Cl (Int (Cl A)) ) by A2, PRE_TOPC:18, TOPS_1:16; ::_thesis: verum end; given B being Subset of T such that A3: B is regular_open and A4: B c= A and A5: A c= Cl B ; ::_thesis: A is condensed A6: Int (Cl B) = B by A3, TOPS_1:def_8; Int B c= Int A by A4, TOPS_1:19; then A7: Cl (Int B) c= Cl (Int A) by PRE_TOPC:19; A8: Cl (Int B) = Cl B by A3, Def2; Int A c= Int (Cl B) by A5, TOPS_1:19; then Cl (Int A) c= Cl B by A6, PRE_TOPC:19; then A9: Cl B = Cl (Int A) by A7, A8, XBOOLE_0:def_10; Cl B c= Cl A by A4, PRE_TOPC:19; then A10: Int (Cl B) c= Int (Cl A) by TOPS_1:19; Cl A c= Cl (Cl B) by A5, PRE_TOPC:19; then Int (Cl A) c= Int (Cl (Cl B)) by TOPS_1:19; then B = Int (Cl A) by A6, A10, XBOOLE_0:def_10; hence A is condensed by A4, A5, A9, Th10; ::_thesis: verum end; theorem :: ISOMICHI:19 for T being TopSpace for A being Subset of T holds ( A is condensed iff ex B being Subset of T st ( B is regular_closed & Int B c= A & A c= B ) ) proof let T be TopSpace; ::_thesis: for A being Subset of T holds ( A is condensed iff ex B being Subset of T st ( B is regular_closed & Int B c= A & A c= B ) ) let A be Subset of T; ::_thesis: ( A is condensed iff ex B being Subset of T st ( B is regular_closed & Int B c= A & A c= B ) ) thus ( A is condensed implies ex B being Subset of T st ( B is regular_closed & Int B c= A & A c= B ) ) ::_thesis: ( ex B being Subset of T st ( B is regular_closed & Int B c= A & A c= B ) implies A is condensed ) proof assume A1: A is condensed ; ::_thesis: ex B being Subset of T st ( B is regular_closed & Int B c= A & A c= B ) then A2: Cl (Int A) = Cl A by Def3; take Cl (Int A) ; ::_thesis: ( Cl (Int A) is regular_closed & Int (Cl (Int A)) c= A & A c= Cl (Int A) ) Int (Cl A) = Int A by A1, Def3; hence ( Cl (Int A) is regular_closed & Int (Cl (Int A)) c= A & A c= Cl (Int A) ) by A2, PRE_TOPC:18, TOPS_1:16; ::_thesis: verum end; given B being Subset of T such that A3: B is regular_closed and A4: Int B c= A and A5: A c= B ; ::_thesis: A is condensed A6: Cl (Int B) = B by A3, TOPS_1:def_7; Cl A c= Cl B by A5, PRE_TOPC:19; then Int (Cl A) c= Int (Cl B) by TOPS_1:19; then A7: Int (Cl A) c= Int B by A3, Def1; Cl (Int B) c= Cl A by A4, PRE_TOPC:19; then Int B c= Int (Cl A) by A6, TOPS_1:19; then A8: Int B = Int (Cl A) by A7, XBOOLE_0:def_10; Int A c= Int B by A5, TOPS_1:19; then A9: Cl (Int A) c= Cl (Int B) by PRE_TOPC:19; Int (Int B) c= Int A by A4, TOPS_1:19; then Cl (Int (Int B)) c= Cl (Int A) by PRE_TOPC:19; then Cl (Int A) = B by A6, A9, XBOOLE_0:def_10; hence A is condensed by A4, A5, A8, Th10; ::_thesis: verum end; begin definition let T be TopStruct ; let A be Subset of T; redefine func Fr A equals :: ISOMICHI:def 4 (Cl A) \ (Int A); compatibility for b1 being Element of bool the carrier of T holds ( b1 = Fr A iff b1 = (Cl A) \ (Int A) ) by TOPGEN_1:8; end; :: deftheorem defines Fr ISOMICHI:def_4_:_ for T being TopStruct for A being Subset of T holds Fr A = (Cl A) \ (Int A); theorem :: ISOMICHI:20 for T being TopSpace for A being Subset of T holds ( A is condensed iff ( Fr A = (Cl (Int A)) \ (Int (Cl A)) & Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) ) ) proof let T be TopSpace; ::_thesis: for A being Subset of T holds ( A is condensed iff ( Fr A = (Cl (Int A)) \ (Int (Cl A)) & Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) ) ) let A be Subset of T; ::_thesis: ( A is condensed iff ( Fr A = (Cl (Int A)) \ (Int (Cl A)) & Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) ) ) A1: A c= Cl A by PRE_TOPC:18; (Cl (Int A)) /\ (Cl (Int (A `))) c= Cl (Int A) by XBOOLE_1:17; then A2: (Int A) \/ ((Cl (Int A)) /\ (Cl (Int (A `)))) c= (Int A) \/ (Cl (Int A)) by XBOOLE_1:13; thus ( A is condensed implies ( Fr A = (Cl (Int A)) \ (Int (Cl A)) & Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) ) ) ::_thesis: ( Fr A = (Cl (Int A)) \ (Int (Cl A)) & Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) implies A is condensed ) proof assume A3: A is condensed ; ::_thesis: ( Fr A = (Cl (Int A)) \ (Int (Cl A)) & Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) ) then A ` is condensed by TDLAT_1:16; then A4: Cl (Int (A `)) = Cl (A `) by Def2; Cl (Int A) = Cl A by A3, Def2; hence ( Fr A = (Cl (Int A)) \ (Int (Cl A)) & Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) ) by A3, A4, Def1, TOPS_1:def_2; ::_thesis: verum end; assume that Fr A = (Cl (Int A)) \ (Int (Cl A)) and A5: Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) ; ::_thesis: A is condensed A6: (Cl A) \/ (Int A) = (Int A) \/ (Fr A) by XBOOLE_1:39; Int A c= A by TOPS_1:16; then Cl A = (Int A) \/ ((Cl (Int A)) /\ (Cl (Int (A `)))) by A5, A1, A6, XBOOLE_1:1, XBOOLE_1:12; then A7: Cl A c= Cl (Int A) by A2, PRE_TOPC:18, XBOOLE_1:12; Cl (Int A) c= Cl A by PRE_TOPC:19, TOPS_1:16; then Cl (Int A) = Cl A by A7, XBOOLE_0:def_10; then A8: A is subcondensed by Def2; A9: A ` c= Cl (A `) by PRE_TOPC:18; A10: (Cl (A `)) \/ (Int (A `)) = (Int (A `)) \/ (Fr (A `)) by XBOOLE_1:39; A11: Fr A = Fr (A `) by TOPS_1:29; (Cl (Int (A `))) /\ (Cl (Int ((A `) `))) c= Cl (Int (A `)) by XBOOLE_1:17; then A12: (Int (A `)) \/ ((Cl (Int (A `))) /\ (Cl (Int ((A `) `)))) c= (Int (A `)) \/ (Cl (Int (A `))) by XBOOLE_1:13; A13: Cl (Int (A `)) c= Cl (A `) by PRE_TOPC:19, TOPS_1:16; A14: Cl (Int (A `)) = Cl ((Cl A) `) by TDLAT_3:3 .= (Int (Cl A)) ` by TDLAT_3:2 ; A15: (Int (A `)) \/ (Cl (Int (A `))) = Cl (Int (A `)) by PRE_TOPC:18, XBOOLE_1:12; Int (A `) c= A ` by TOPS_1:16; then Cl (A `) = (Int (A `)) \/ ((Cl (Int (A `))) /\ (Cl (Int ((A `) `)))) by A5, A9, A11, A10, XBOOLE_1:1, XBOOLE_1:12; then A16: Cl (A `) = Cl (Int (A `)) by A13, A12, A15, XBOOLE_0:def_10; Cl (A `) = (Int A) ` by TDLAT_3:2; then Int A = ((Int (Cl A)) `) ` by A16, A14; then A is supercondensed by Def1; hence A is condensed by A8; ::_thesis: verum end; definition let T be TopStruct ; let A be Subset of T; func Border A -> Subset of T equals :: ISOMICHI:def 5 Int (Fr A); coherence Int (Fr A) is Subset of T ; end; :: deftheorem defines Border ISOMICHI:def_5_:_ for T being TopStruct for A being Subset of T holds Border A = Int (Fr A); theorem Th21: :: ISOMICHI:21 for T being TopSpace for A being Subset of T holds ( Border A is regular_open & Border A = (Int (Cl A)) \ (Cl (Int A)) & Border A = (Int (Cl A)) /\ (Int (Cl (A `))) ) proof let T be TopSpace; ::_thesis: for A being Subset of T holds ( Border A is regular_open & Border A = (Int (Cl A)) \ (Cl (Int A)) & Border A = (Int (Cl A)) /\ (Int (Cl (A `))) ) let A be Subset of T; ::_thesis: ( Border A is regular_open & Border A = (Int (Cl A)) \ (Cl (Int A)) & Border A = (Int (Cl A)) /\ (Int (Cl (A `))) ) Fr A = Cl (Fr A) by PRE_TOPC:22; hence Border A is regular_open ; ::_thesis: ( Border A = (Int (Cl A)) \ (Cl (Int A)) & Border A = (Int (Cl A)) /\ (Int (Cl (A `))) ) (Int (Cl A)) \ (Cl (Int A)) = (Int (Cl A)) \ (((Cl (Int A)) `) `) .= (Int (Cl A)) \ ((Int ((Int A) `)) `) by TDLAT_3:3 .= (Int (Cl A)) \ ((Int (Cl (A `))) `) by TDLAT_3:2 .= (Int (Cl A)) /\ (((Int (Cl (A `))) `) `) by SUBSET_1:13 .= Int ((Cl A) /\ (Cl (A `))) by TOPS_1:17 .= Int (Fr A) by TOPS_1:def_2 ; hence Border A = (Int (Cl A)) \ (Cl (Int A)) ; ::_thesis: Border A = (Int (Cl A)) /\ (Int (Cl (A `))) (Int (Cl A)) /\ (Int (Cl (A `))) = Int ((Cl A) /\ (Cl (A `))) by TOPS_1:17 .= Int (Fr A) by TOPS_1:def_2 ; hence Border A = (Int (Cl A)) /\ (Int (Cl (A `))) ; ::_thesis: verum end; registration let T be TopSpace; let A be Subset of T; cluster Border A -> regular_open ; coherence Border A is regular_open by Th21; end; theorem Th22: :: ISOMICHI:22 for T being TopSpace for A being Subset of T holds ( A is supercondensed iff ( Int A is regular_open & Border A is empty ) ) proof let T be TopSpace; ::_thesis: for A being Subset of T holds ( A is supercondensed iff ( Int A is regular_open & Border A is empty ) ) let A be Subset of T; ::_thesis: ( A is supercondensed iff ( Int A is regular_open & Border A is empty ) ) A1: Int A c= Int (Cl A) by PRE_TOPC:18, TOPS_1:19; thus ( A is supercondensed implies ( Int A is regular_open & Border A is empty ) ) ::_thesis: ( Int A is regular_open & Border A is empty implies A is supercondensed ) proof assume A2: A is supercondensed ; ::_thesis: ( Int A is regular_open & Border A is empty ) then Int (Cl A) = Int A by Def1; then Int (Cl A) c= Cl (Int A) by PRE_TOPC:18; then (Int (Cl A)) \ (Cl (Int A)) is empty by XBOOLE_1:37; hence ( Int A is regular_open & Border A is empty ) by A2, Def1, Th21; ::_thesis: verum end; assume that A3: Int A is regular_open and A4: Border A is empty ; ::_thesis: A is supercondensed (Int (Cl A)) \ (Cl (Int A)) is empty by A4, Th21; then Int (Cl A) c= Cl (Int A) by XBOOLE_1:37; then A5: Int (Int (Cl A)) c= Int (Cl (Int A)) by TOPS_1:19; Int A = Int (Cl (Int A)) by A3, TOPS_1:def_8; then Int (Cl A) = Int A by A5, A1, XBOOLE_0:def_10; hence A is supercondensed by Def1; ::_thesis: verum end; theorem Th23: :: ISOMICHI:23 for T being TopSpace for A being Subset of T holds ( A is subcondensed iff ( Cl A is regular_closed & Border A is empty ) ) proof let T be TopSpace; ::_thesis: for A being Subset of T holds ( A is subcondensed iff ( Cl A is regular_closed & Border A is empty ) ) let A be Subset of T; ::_thesis: ( A is subcondensed iff ( Cl A is regular_closed & Border A is empty ) ) A1: Cl (Int A) c= Cl A by PRE_TOPC:19, TOPS_1:16; thus ( A is subcondensed implies ( Cl A is regular_closed & Border A is empty ) ) ::_thesis: ( Cl A is regular_closed & Border A is empty implies A is subcondensed ) proof assume A2: A is subcondensed ; ::_thesis: ( Cl A is regular_closed & Border A is empty ) then Cl (Int A) = Cl A by Def2; then Int (Cl A) c= Cl (Int A) by TOPS_1:16; then (Int (Cl A)) \ (Cl (Int A)) is empty by XBOOLE_1:37; hence ( Cl A is regular_closed & Border A is empty ) by A2, Def2, Th21; ::_thesis: verum end; assume that A3: Cl A is regular_closed and A4: Border A is empty ; ::_thesis: A is subcondensed (Int (Cl A)) \ (Cl (Int A)) is empty by A4, Th21; then Int (Cl A) c= Cl (Int A) by XBOOLE_1:37; then A5: Cl (Int (Cl A)) c= Cl (Cl (Int A)) by PRE_TOPC:19; Cl A = Cl (Int (Cl A)) by A3, TOPS_1:def_7; then Cl (Int A) = Cl A by A5, A1, XBOOLE_0:def_10; hence A is subcondensed by Def2; ::_thesis: verum end; registration let T be TopSpace; let A be Subset of T; cluster Border (Border A) -> empty ; coherence Border (Border A) is empty ; end; theorem :: ISOMICHI:24 for T being TopSpace for A being Subset of T holds ( A is condensed iff ( Int A is regular_open & Cl A is regular_closed & Border A is empty ) ) proof let T be TopSpace; ::_thesis: for A being Subset of T holds ( A is condensed iff ( Int A is regular_open & Cl A is regular_closed & Border A is empty ) ) let A be Subset of T; ::_thesis: ( A is condensed iff ( Int A is regular_open & Cl A is regular_closed & Border A is empty ) ) thus ( A is condensed implies ( Int A is regular_open & Cl A is regular_closed & Border A is empty ) ) by Th22, Th23; ::_thesis: ( Int A is regular_open & Cl A is regular_closed & Border A is empty implies A is condensed ) assume that A1: Int A is regular_open and A2: Cl A is regular_closed and A3: Border A is empty ; ::_thesis: A is condensed A4: A is subcondensed by A2, A3, Th23; A is supercondensed by A1, A3, Th22; hence A is condensed by A4; ::_thesis: verum end; begin theorem :: ISOMICHI:25 for A being Subset of R^1 for a being real number st A = ].-infty,a.] holds Int A = ].-infty,a.[ proof let A be Subset of R^1; ::_thesis: for a being real number st A = ].-infty,a.] holds Int A = ].-infty,a.[ let a be real number ; ::_thesis: ( A = ].-infty,a.] implies Int A = ].-infty,a.[ ) assume A = ].-infty,a.] ; ::_thesis: Int A = ].-infty,a.[ then A ` = ].a,+infty.[ by TOPMETR:17, XXREAL_1:224, XXREAL_1:288; then Cl (A `) = [.a,+infty.[ by BORSUK_5:49; then (Cl (A `)) ` = ].-infty,a.[ by TOPMETR:17, XXREAL_1:224, XXREAL_1:294; hence Int A = ].-infty,a.[ by TOPS_1:def_1; ::_thesis: verum end; theorem :: ISOMICHI:26 for A being Subset of R^1 for a being real number st A = [.a,+infty.[ holds Int A = ].a,+infty.[ proof let A be Subset of R^1; ::_thesis: for a being real number st A = [.a,+infty.[ holds Int A = ].a,+infty.[ let a be real number ; ::_thesis: ( A = [.a,+infty.[ implies Int A = ].a,+infty.[ ) assume A = [.a,+infty.[ ; ::_thesis: Int A = ].a,+infty.[ then A ` = ].-infty,a.[ by TOPMETR:17, XXREAL_1:224, XXREAL_1:294; then Cl (A `) = ].-infty,a.] by BORSUK_5:51; then (Cl (A `)) ` = ].a,+infty.[ by TOPMETR:17, XXREAL_1:224, XXREAL_1:288; hence Int A = ].a,+infty.[ by TOPS_1:def_1; ::_thesis: verum end; theorem Th27: :: ISOMICHI:27 for A being Subset of R^1 for a, b being real number st A = (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ holds Cl A = the carrier of R^1 proof reconsider B = IRRAT as Subset of R^1 by TOPMETR:17; let A be Subset of R^1; ::_thesis: for a, b being real number st A = (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ holds Cl A = the carrier of R^1 let a, b be real number ; ::_thesis: ( A = (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ implies Cl A = the carrier of R^1 ) assume A1: A = (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ ; ::_thesis: Cl A = the carrier of R^1 B c= A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in A ) assume A2: x in B ; ::_thesis: x in A then reconsider x9 = x as real number ; percases ( x9 <= a or ( x9 > a & x9 < b ) or x9 >= b ) ; suppose x9 <= a ; ::_thesis: x in A then x9 in ].-infty,a.] by XXREAL_1:234; then x9 in ].-infty,a.] \/ (IRRAT (a,b)) by XBOOLE_0:def_3; hence x in A by A1, XBOOLE_0:def_3; ::_thesis: verum end; suppose ( x9 > a & x9 < b ) ; ::_thesis: x in A then x9 in ].a,b.[ by XXREAL_1:4; then x9 in IRRAT /\ ].a,b.[ by A2, XBOOLE_0:def_4; then x9 in IRRAT (a,b) by BORSUK_5:def_3; then x9 in ].-infty,a.] \/ (IRRAT (a,b)) by XBOOLE_0:def_3; hence x in A by A1, XBOOLE_0:def_3; ::_thesis: verum end; suppose x9 >= b ; ::_thesis: x in A then x9 in [.b,+infty.[ by XXREAL_1:236; hence x in A by A1, XBOOLE_0:def_3; ::_thesis: verum end; end; end; then A3: Cl B c= Cl A by PRE_TOPC:19; Cl B = the carrier of R^1 by BORSUK_5:28; hence Cl A = the carrier of R^1 by A3, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: ISOMICHI:28 for A being Subset of R^1 for a, b being real number st A = RAT (a,b) holds Int A = {} proof let A be Subset of R^1; ::_thesis: for a, b being real number st A = RAT (a,b) holds Int A = {} let a, b be real number ; ::_thesis: ( A = RAT (a,b) implies Int A = {} ) assume A1: A = RAT (a,b) ; ::_thesis: Int A = {} A ` = REAL \ A by TOPMETR:17 .= (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ by A1, BORSUK_5:58 ; then Cl (A `) = [#] R^1 by Th27; then (Cl (A `)) ` = {} R^1 by XBOOLE_1:37; hence Int A = {} by TOPS_1:def_1; ::_thesis: verum end; theorem :: ISOMICHI:29 for A being Subset of R^1 for a, b being real number st A = IRRAT (a,b) holds Int A = {} proof reconsider B = IRRAT as Subset of R^1 by TOPMETR:17; let A be Subset of R^1; ::_thesis: for a, b being real number st A = IRRAT (a,b) holds Int A = {} let a, b be real number ; ::_thesis: ( A = IRRAT (a,b) implies Int A = {} ) assume A = IRRAT (a,b) ; ::_thesis: Int A = {} then A = IRRAT /\ ].a,b.[ by BORSUK_5:def_3; then A c= B by XBOOLE_1:17; then A is boundary by TOPGEN_1:54, TOPS_3:11; hence Int A = {} ; ::_thesis: verum end; theorem :: ISOMICHI:30 for a, b being real number st a >= b holds IRRAT (a,b) = {} proof let a, b be real number ; ::_thesis: ( a >= b implies IRRAT (a,b) = {} ) assume A1: a >= b ; ::_thesis: IRRAT (a,b) = {} IRRAT (a,b) = IRRAT /\ ].a,b.[ by BORSUK_5:def_3 .= IRRAT /\ {} by A1, XXREAL_1:28 ; hence IRRAT (a,b) = {} ; ::_thesis: verum end; theorem Th31: :: ISOMICHI:31 for a, b being real number holds IRRAT (a,b) c= [.a,+infty.[ proof let a, b be real number ; ::_thesis: IRRAT (a,b) c= [.a,+infty.[ let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in IRRAT (a,b) or x in [.a,+infty.[ ) assume A1: x in IRRAT (a,b) ; ::_thesis: x in [.a,+infty.[ then reconsider x = x as real number ; a < x by A1, BORSUK_5:30; hence x in [.a,+infty.[ by XXREAL_1:236; ::_thesis: verum end; theorem Th32: :: ISOMICHI:32 for A being Subset of R^1 for a, b, c being real number st A = ].-infty,a.[ \/ (RAT (b,c)) & a < b & b < c holds Int A = ].-infty,a.[ proof let A be Subset of R^1; ::_thesis: for a, b, c being real number st A = ].-infty,a.[ \/ (RAT (b,c)) & a < b & b < c holds Int A = ].-infty,a.[ let a, b, c be real number ; ::_thesis: ( A = ].-infty,a.[ \/ (RAT (b,c)) & a < b & b < c implies Int A = ].-infty,a.[ ) reconsider B = [.a,b.], C = IRRAT (b,c), D = [.c,+infty.[ as Subset of R^1 by TOPMETR:17; assume that A1: A = ].-infty,a.[ \/ (RAT (b,c)) and A2: a < b and A3: b < c ; ::_thesis: Int A = ].-infty,a.[ A4: a < c by A2, A3, XXREAL_0:2; A ` = REAL \ (].-infty,a.[ \/ (RAT (b,c))) by A1, TOPMETR:17 .= (REAL \ (RAT (b,c))) \ ].-infty,a.[ by XBOOLE_1:41 .= ((].-infty,b.] \/ (IRRAT (b,c))) \/ [.c,+infty.[) \ ].-infty,a.[ by BORSUK_5:58 .= (].-infty,b.] \/ ((IRRAT (b,c)) \/ [.c,+infty.[)) \ ].-infty,a.[ by XBOOLE_1:4 .= (].-infty,b.] \ ].-infty,a.[) \/ (((IRRAT (b,c)) \/ [.c,+infty.[) \ ].-infty,a.[) by XBOOLE_1:42 ; then A5: A ` = [.a,b.] \/ (((IRRAT (b,c)) \/ [.c,+infty.[) \ ].-infty,a.[) by XXREAL_1:289 .= [.a,b.] \/ (((IRRAT (b,c)) \ ].-infty,a.[) \/ ([.c,+infty.[ \ ].-infty,a.[)) by XBOOLE_1:42 ; right_closed_halfline c is closed ; then D is closed by JORDAN5A:23; then A6: Cl D = D by PRE_TOPC:22; [.b,+infty.[ misses ].-infty,a.[ by A2, XXREAL_1:94; then IRRAT (b,c) misses ].-infty,a.[ by Th31, XBOOLE_1:63; then A7: (IRRAT (b,c)) \ ].-infty,a.[ = IRRAT (b,c) by XBOOLE_1:83; B is closed by JORDAN5A:23; then A8: Cl B = B by PRE_TOPC:22; [.c,+infty.[ misses ].-infty,a.[ by A2, A3, XXREAL_0:2, XXREAL_1:94; then A ` = [.a,b.] \/ ((IRRAT (b,c)) \/ [.c,+infty.[) by A5, A7, XBOOLE_1:83 .= [.a,b.] \/ ((IRRAT (b,c)) \/ ({c} \/ ].c,+infty.[)) by BORSUK_5:43 .= ([.a,b.] \/ (IRRAT (b,c))) \/ ({c} \/ ].c,+infty.[) by XBOOLE_1:4 .= ([.a,b.] \/ (IRRAT (b,c))) \/ [.c,+infty.[ by BORSUK_5:43 ; then Cl (A `) = (Cl (B \/ C)) \/ (Cl D) by PRE_TOPC:20 .= ((Cl B) \/ (Cl C)) \/ (Cl D) by PRE_TOPC:20 .= (B \/ [.b,c.]) \/ D by A8, A6, A3, BORSUK_5:32 .= [.a,c.] \/ D by A2, A3, XXREAL_1:165 .= [.a,+infty.[ by A4, BORSUK_5:11 ; then (Cl (A `)) ` = ].-infty,a.[ by TOPMETR:17, XXREAL_1:224, XXREAL_1:294; hence Int A = ].-infty,a.[ by TOPS_1:def_1; ::_thesis: verum end; Lm1: for a, b being real number st a < b holds [.a,b.] \/ {b} = [.a,b.] proof let a, b be real number ; ::_thesis: ( a < b implies [.a,b.] \/ {b} = [.a,b.] ) assume A1: a < b ; ::_thesis: [.a,b.] \/ {b} = [.a,b.] then [.a,b.] = [.a,b.[ \/ {b} by XXREAL_1:129 .= ([.a,b.[ \/ {b}) \/ {b} by XBOOLE_1:6 ; hence [.a,b.] \/ {b} = [.a,b.] by A1, XXREAL_1:129; ::_thesis: verum end; theorem :: ISOMICHI:33 for a, b being real number st a < b holds REAL = (].-infty,a.[ \/ [.a,b.]) \/ ].b,+infty.[ proof let a, b be real number ; ::_thesis: ( a < b implies REAL = (].-infty,a.[ \/ [.a,b.]) \/ ].b,+infty.[ ) assume A1: a < b ; ::_thesis: REAL = (].-infty,a.[ \/ [.a,b.]) \/ ].b,+infty.[ REAL = (REAL \ {a}) \/ {a} by XBOOLE_1:45 .= (].-infty,a.[ \/ ].a,+infty.[) \/ {a} by XXREAL_1:389 .= ].-infty,a.[ \/ (].a,+infty.[ \/ {a}) by XBOOLE_1:4 .= ].-infty,a.[ \/ [.a,+infty.[ by BORSUK_5:43 .= ].-infty,a.[ \/ ([.a,b.] \/ [.b,+infty.[) by A1, BORSUK_5:11 .= ].-infty,a.[ \/ ([.a,b.] \/ ({b} \/ ].b,+infty.[)) by BORSUK_5:43 .= ].-infty,a.[ \/ (([.a,b.] \/ {b}) \/ ].b,+infty.[) by XBOOLE_1:4 .= (].-infty,a.[ \/ ([.a,b.] \/ {b})) \/ ].b,+infty.[ by XBOOLE_1:4 ; hence REAL = (].-infty,a.[ \/ [.a,b.]) \/ ].b,+infty.[ by A1, Lm1; ::_thesis: verum end; theorem Th34: :: ISOMICHI:34 for A being Subset of R^1 for a, b, c being real number st A = ].-infty,a.] \/ [.b,c.] & a < b & b < c holds Int A = ].-infty,a.[ \/ ].b,c.[ proof let A be Subset of R^1; ::_thesis: for a, b, c being real number st A = ].-infty,a.] \/ [.b,c.] & a < b & b < c holds Int A = ].-infty,a.[ \/ ].b,c.[ let a, b, c be real number ; ::_thesis: ( A = ].-infty,a.] \/ [.b,c.] & a < b & b < c implies Int A = ].-infty,a.[ \/ ].b,c.[ ) assume that A1: A = ].-infty,a.] \/ [.b,c.] and A2: a < b and A3: b < c ; ::_thesis: Int A = ].-infty,a.[ \/ ].b,c.[ a < c by A2, A3, XXREAL_0:2; then A4: ].c,+infty.[ /\ ].a,+infty.[ = ].c,+infty.[ by XBOOLE_1:28, XXREAL_1:46; reconsider B = ].a,b.[, C = ].c,+infty.[ as Subset of R^1 by TOPMETR:17; A5: Cl B = [.a,b.] by A2, BORSUK_5:16; A6: Cl C = [.c,+infty.[ by BORSUK_5:49; A ` = REAL \ (].-infty,a.] \/ [.b,c.]) by A1, TOPMETR:17 .= (REAL \ (left_closed_halfline a)) \ [.b,c.] by XBOOLE_1:41 .= (right_open_halfline a) \ [.b,c.] by XXREAL_1:224, XXREAL_1:288 .= ].a,+infty.[ \ ([.b,+infty.[ \ ].c,+infty.[) by XXREAL_1:295 .= (].a,+infty.[ \ [.b,+infty.[) \/ (].a,+infty.[ /\ ].c,+infty.[) by XBOOLE_1:52 .= ].a,b.[ \/ ].c,+infty.[ by A4, XXREAL_1:294 ; then (Cl (A `)) ` = REAL \ ([.c,+infty.[ \/ [.a,b.]) by A5, A6, PRE_TOPC:20, TOPMETR:17 .= (REAL \ (right_closed_halfline c)) \ [.a,b.] by XBOOLE_1:41 .= (left_open_halfline c) \ [.a,b.] by XXREAL_1:224, XXREAL_1:294 .= ].-infty,a.[ \/ ].b,c.[ by A2, A3, XXREAL_0:2, XXREAL_1:339 ; hence Int A = ].-infty,a.[ \/ ].b,c.[ by TOPS_1:def_1; ::_thesis: verum end; begin notation let A, B be set ; antonym A,B are_c=-incomparable for A,B are_c=-comparable ; end; theorem Th35: :: ISOMICHI:35 for A, B being set holds ( A,B are_c=-incomparable or A c= B or B c< A ) proof let A, B be set ; ::_thesis: ( A,B are_c=-incomparable or A c= B or B c< A ) assume that A1: A,B are_c=-comparable and A2: not A c= B and A3: not B c< A ; ::_thesis: contradiction ( A c= B or B c= A ) by A1, XBOOLE_0:def_9; hence contradiction by A2, A3, XBOOLE_0:def_8; ::_thesis: verum end; definition let T be TopSpace; let A be Subset of T; attrA is 1st_class means :Def6: :: ISOMICHI:def 6 Int (Cl A) c= Cl (Int A); attrA is 2nd_class means :Def7: :: ISOMICHI:def 7 Cl (Int A) c< Int (Cl A); attrA is 3rd_class means :Def8: :: ISOMICHI:def 8 Cl (Int A), Int (Cl A) are_c=-incomparable ; end; :: deftheorem Def6 defines 1st_class ISOMICHI:def_6_:_ for T being TopSpace for A being Subset of T holds ( A is 1st_class iff Int (Cl A) c= Cl (Int A) ); :: deftheorem Def7 defines 2nd_class ISOMICHI:def_7_:_ for T being TopSpace for A being Subset of T holds ( A is 2nd_class iff Cl (Int A) c< Int (Cl A) ); :: deftheorem Def8 defines 3rd_class ISOMICHI:def_8_:_ for T being TopSpace for A being Subset of T holds ( A is 3rd_class iff Cl (Int A), Int (Cl A) are_c=-incomparable ); theorem :: ISOMICHI:36 for T being TopSpace for A being Subset of T holds ( A is 1st_class or A is 2nd_class or A is 3rd_class ) proof let T be TopSpace; ::_thesis: for A being Subset of T holds ( A is 1st_class or A is 2nd_class or A is 3rd_class ) let A be Subset of T; ::_thesis: ( A is 1st_class or A is 2nd_class or A is 3rd_class ) assume that A1: not A is 1st_class and A2: not A is 2nd_class and A3: not A is 3rd_class ; ::_thesis: contradiction A4: not Cl (Int A) c< Int (Cl A) by A2, Def7; A5: Cl (Int A), Int (Cl A) are_c=-comparable by A3, Def8; not Int (Cl A) c= Cl (Int A) by A1, Def6; hence contradiction by A4, A5, Th35; ::_thesis: verum end; registration let T be TopSpace; cluster 1st_class -> non 2nd_class non 3rd_class for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is 1st_class holds ( not b1 is 2nd_class & not b1 is 3rd_class ) proof let A be Subset of T; ::_thesis: ( A is 1st_class implies ( not A is 2nd_class & not A is 3rd_class ) ) assume A is 1st_class ; ::_thesis: ( not A is 2nd_class & not A is 3rd_class ) then A1: Int (Cl A) c= Cl (Int A) by Def6; then A2: Cl (Int A), Int (Cl A) are_c=-comparable by XBOOLE_0:def_9; not Cl (Int A) c< Int (Cl A) by A1, XBOOLE_1:60; hence ( not A is 2nd_class & not A is 3rd_class ) by A2, Def7, Def8; ::_thesis: verum end; cluster 2nd_class -> non 1st_class non 3rd_class for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is 2nd_class holds ( not b1 is 1st_class & not b1 is 3rd_class ) proof let A be Subset of T; ::_thesis: ( A is 2nd_class implies ( not A is 1st_class & not A is 3rd_class ) ) assume A is 2nd_class ; ::_thesis: ( not A is 1st_class & not A is 3rd_class ) then A3: Cl (Int A) c< Int (Cl A) by Def7; then Cl (Int A) c= Int (Cl A) by XBOOLE_0:def_8; then A4: Cl (Int A), Int (Cl A) are_c=-comparable by XBOOLE_0:def_9; not Int (Cl A) c= Cl (Int A) by A3, XBOOLE_0:def_8; hence ( not A is 1st_class & not A is 3rd_class ) by A4, Def6, Def8; ::_thesis: verum end; cluster 3rd_class -> non 1st_class non 2nd_class for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is 3rd_class holds ( not b1 is 1st_class & not b1 is 2nd_class ) ; end; theorem Th37: :: ISOMICHI:37 for T being TopSpace for A being Subset of T holds ( A is 1st_class iff Border A is empty ) proof let T be TopSpace; ::_thesis: for A being Subset of T holds ( A is 1st_class iff Border A is empty ) let A be Subset of T; ::_thesis: ( A is 1st_class iff Border A is empty ) A1: ( Border A is empty implies A is 1st_class ) proof assume Border A is empty ; ::_thesis: A is 1st_class then (Int (Cl A)) \ (Cl (Int A)) = {} by Th21; then Int (Cl A) c= Cl (Int A) by XBOOLE_1:37; hence A is 1st_class by Def6; ::_thesis: verum end; ( A is 1st_class implies Border A is empty ) proof assume A is 1st_class ; ::_thesis: Border A is empty then Int (Cl A) c= Cl (Int A) by Def6; then (Int (Cl A)) \ (Cl (Int A)) = {} by XBOOLE_1:37; hence Border A is empty by Th21; ::_thesis: verum end; hence ( A is 1st_class iff Border A is empty ) by A1; ::_thesis: verum end; registration let T be TopSpace; cluster supercondensed -> 1st_class for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is supercondensed holds b1 is 1st_class proof let A be Subset of T; ::_thesis: ( A is supercondensed implies A is 1st_class ) assume A is supercondensed ; ::_thesis: A is 1st_class then Border A is empty by Th22; hence A is 1st_class by Th37; ::_thesis: verum end; cluster subcondensed -> 1st_class for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is subcondensed holds b1 is 1st_class proof let A be Subset of T; ::_thesis: ( A is subcondensed implies A is 1st_class ) assume A is subcondensed ; ::_thesis: A is 1st_class then Border A is empty by Th23; hence A is 1st_class by Th37; ::_thesis: verum end; end; definition let T be TopSpace; attrT is with_1st_class_subsets means :Def9: :: ISOMICHI:def 9 ex A being Subset of T st A is 1st_class ; attrT is with_2nd_class_subsets means :Def10: :: ISOMICHI:def 10 ex A being Subset of T st A is 2nd_class ; attrT is with_3rd_class_subsets means :Def11: :: ISOMICHI:def 11 ex A being Subset of T st A is 3rd_class ; end; :: deftheorem Def9 defines with_1st_class_subsets ISOMICHI:def_9_:_ for T being TopSpace holds ( T is with_1st_class_subsets iff ex A being Subset of T st A is 1st_class ); :: deftheorem Def10 defines with_2nd_class_subsets ISOMICHI:def_10_:_ for T being TopSpace holds ( T is with_2nd_class_subsets iff ex A being Subset of T st A is 2nd_class ); :: deftheorem Def11 defines with_3rd_class_subsets ISOMICHI:def_11_:_ for T being TopSpace holds ( T is with_3rd_class_subsets iff ex A being Subset of T st A is 3rd_class ); registration let T be non empty anti-discrete TopSpace; cluster non empty proper -> 2nd_class for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is proper & not b1 is empty holds b1 is 2nd_class proof let A be Subset of T; ::_thesis: ( A is proper & not A is empty implies A is 2nd_class ) assume A1: ( A is proper & not A is empty ) ; ::_thesis: A is 2nd_class then A <> the carrier of T by SUBSET_1:def_6; then Int A = {} by TEX_1:10; then A2: Cl (Int A) = {} by TEX_1:9; Cl A = the carrier of T by A1, TEX_1:9; then Int (Cl A) = the carrier of T by TEX_1:10; then Cl (Int A) c< Int (Cl A) by A2, XBOOLE_0:def_8; hence A is 2nd_class by Def7; ::_thesis: verum end; end; registration let T be non trivial strict anti-discrete TopSpace; cluster 2nd_class for Element of bool the carrier of T; existence ex b1 being Subset of T st b1 is 2nd_class proof set x = the Element of T; reconsider A = { the Element of T} as Subset of T ; Cl A = the carrier of T by TEX_1:9; hence ex b1 being Subset of T st b1 is 2nd_class ; ::_thesis: verum end; end; registration cluster non trivial strict TopSpace-like with_1st_class_subsets with_2nd_class_subsets for TopStruct ; existence ex b1 being TopSpace st ( b1 is with_1st_class_subsets & b1 is with_2nd_class_subsets & b1 is strict & not b1 is trivial ) proof set T = the non trivial strict anti-discrete TopSpace; set B = the 2nd_class Subset of the non trivial strict anti-discrete TopSpace; the 2nd_class Subset of the non trivial strict anti-discrete TopSpace is 2nd_class ; then A1: the non trivial strict anti-discrete TopSpace is with_2nd_class_subsets by Def10; {} the non trivial strict anti-discrete TopSpace is 1st_class ; then the non trivial strict anti-discrete TopSpace is with_1st_class_subsets by Def9; hence ex b1 being TopSpace st ( b1 is with_1st_class_subsets & b1 is with_2nd_class_subsets & b1 is strict & not b1 is trivial ) by A1; ::_thesis: verum end; cluster non empty strict TopSpace-like with_3rd_class_subsets for TopStruct ; existence ex b1 being TopSpace st ( b1 is with_3rd_class_subsets & not b1 is empty & b1 is strict ) proof set B = ].-infty,1.[; set C = RAT (2,4); take R^1 ; ::_thesis: ( R^1 is with_3rd_class_subsets & not R^1 is empty & R^1 is strict ) set A = ].-infty,1.[ \/ (RAT (2,4)); reconsider A = ].-infty,1.[ \/ (RAT (2,4)), B = ].-infty,1.[, C = RAT (2,4) as Subset of R^1 by TOPMETR:17; A2: Cl C = [.2,4.] by BORSUK_5:31; Cl B = ].-infty,1.] by BORSUK_5:51; then Cl A = ].-infty,1.] \/ [.2,4.] by A2, PRE_TOPC:20; then A3: Int (Cl A) = ].-infty,1.[ \/ ].2,4.[ by Th34; A4: Cl (Int A) = ].-infty,1.] by Th32, BORSUK_5:51; 3 in ].2,4.[ by XXREAL_1:4; then 3 in Int (Cl A) by A3, XBOOLE_0:def_3; then A5: not Int (Cl A) c= Cl (Int A) by A4, XXREAL_1:234; A6: not 1 in ].2,4.[ by XXREAL_1:4; A7: not 1 in ].-infty,1.[ by XXREAL_1:4; 1 in Cl (Int A) by A4, XXREAL_1:234; then not Cl (Int A) c= Int (Cl A) by A3, A7, A6, XBOOLE_0:def_3; then Int (Cl A), Cl (Int A) are_c=-incomparable by A5, XBOOLE_0:def_9; then A is 3rd_class by Def8; hence ( R^1 is with_3rd_class_subsets & not R^1 is empty & R^1 is strict ) by Def11; ::_thesis: verum end; end; registration let T be TopSpace; cluster 1st_class for Element of bool the carrier of T; existence ex b1 being Subset of T st b1 is 1st_class proof take {} T ; ::_thesis: {} T is 1st_class thus {} T is 1st_class ; ::_thesis: verum end; end; registration let T be with_2nd_class_subsets TopSpace; cluster 2nd_class for Element of bool the carrier of T; existence ex b1 being Subset of T st b1 is 2nd_class by Def10; end; registration let T be with_3rd_class_subsets TopSpace; cluster 3rd_class for Element of bool the carrier of T; existence ex b1 being Subset of T st b1 is 3rd_class by Def11; end; theorem Th38: :: ISOMICHI:38 for T being TopSpace for A being Subset of T holds ( A is 1st_class iff A ` is 1st_class ) proof let T be TopSpace; ::_thesis: for A being Subset of T holds ( A is 1st_class iff A ` is 1st_class ) let A be Subset of T; ::_thesis: ( A is 1st_class iff A ` is 1st_class ) A1: ( A ` is 1st_class implies A is 1st_class ) proof assume A ` is 1st_class ; ::_thesis: A is 1st_class then Int (Cl (A `)) c= Cl (Int (A `)) by Def6; then Int ((Int A) `) c= Cl (Int (A `)) by TDLAT_3:2; then (Cl (Int A)) ` c= Cl (Int (A `)) by TDLAT_3:3; then (Cl (Int A)) ` c= Cl ((Cl A) `) by TDLAT_3:3; then (Cl (Int A)) ` c= (Int (Cl A)) ` by TDLAT_3:2; then Int (Cl A) c= Cl (Int A) by SUBSET_1:12; hence A is 1st_class by Def6; ::_thesis: verum end; ( A is 1st_class implies A ` is 1st_class ) proof assume A is 1st_class ; ::_thesis: A ` is 1st_class then Int (Cl A) c= Cl (Int A) by Def6; then (Cl (Int A)) ` c= (Int (Cl A)) ` by SUBSET_1:12; then Int ((Int A) `) c= (Int (Cl A)) ` by TDLAT_3:3; then Int ((Int A) `) c= Cl ((Cl A) `) by TDLAT_3:2; then Int ((Int A) `) c= Cl (Int (A `)) by TDLAT_3:3; then Int (Cl (A `)) c= Cl (Int (A `)) by TDLAT_3:2; hence A ` is 1st_class by Def6; ::_thesis: verum end; hence ( A is 1st_class iff A ` is 1st_class ) by A1; ::_thesis: verum end; theorem Th39: :: ISOMICHI:39 for T being TopSpace for A being Subset of T holds ( A is 2nd_class iff A ` is 2nd_class ) proof let T be TopSpace; ::_thesis: for A being Subset of T holds ( A is 2nd_class iff A ` is 2nd_class ) let A be Subset of T; ::_thesis: ( A is 2nd_class iff A ` is 2nd_class ) A1: for A being Subset of T st A ` is 2nd_class holds A is 2nd_class proof let A be Subset of T; ::_thesis: ( A ` is 2nd_class implies A is 2nd_class ) assume A ` is 2nd_class ; ::_thesis: A is 2nd_class then A2: Cl (Int (A `)) c< Int (Cl (A `)) by Def7; then Cl (Int (A `)) c= Int (Cl (A `)) by XBOOLE_0:def_8; then Cl (Int (A `)) c= Int ((Int A) `) by TDLAT_3:2; then Cl (Int (A `)) c= (Cl (Int A)) ` by TDLAT_3:3; then Cl ((Cl A) `) c= (Cl (Int A)) ` by TDLAT_3:3; then (Int (Cl A)) ` c= (Cl (Int A)) ` by TDLAT_3:2; then A3: Cl (Int A) c= Int (Cl A) by SUBSET_1:12; Cl ((Cl A) `) <> Int (Cl (A `)) by A2, TDLAT_3:3; then Cl ((Cl A) `) <> Int ((Int A) `) by TDLAT_3:2; then (Cl (Int A)) ` <> Cl ((Cl A) `) by TDLAT_3:3; then Cl (Int A) <> Int (Cl A) by TDLAT_3:2; then Cl (Int A) c< Int (Cl A) by A3, XBOOLE_0:def_8; hence A is 2nd_class by Def7; ::_thesis: verum end; ( A is 2nd_class implies A ` is 2nd_class ) proof assume A is 2nd_class ; ::_thesis: A ` is 2nd_class then (A `) ` is 2nd_class ; hence A ` is 2nd_class by A1; ::_thesis: verum end; hence ( A is 2nd_class iff A ` is 2nd_class ) by A1; ::_thesis: verum end; theorem Th40: :: ISOMICHI:40 for T being TopSpace for A being Subset of T holds ( A is 3rd_class iff A ` is 3rd_class ) proof let T be TopSpace; ::_thesis: for A being Subset of T holds ( A is 3rd_class iff A ` is 3rd_class ) let A be Subset of T; ::_thesis: ( A is 3rd_class iff A ` is 3rd_class ) (Int (Cl A)) ` = Cl ((Cl A) `) by TDLAT_3:2 .= Cl (Int (A `)) by TDLAT_3:3 ; then A1: Int (Cl A) = (Cl (Int (A `))) ` ; (Cl (Int A)) ` = Int ((Int A) `) by TDLAT_3:3 .= Int (Cl (A `)) by TDLAT_3:2 ; then A2: Cl (Int A) = (Int (Cl (A `))) ` ; A3: ( A ` is 3rd_class implies A is 3rd_class ) proof assume A ` is 3rd_class ; ::_thesis: A is 3rd_class then A4: Cl (Int (A `)), Int (Cl (A `)) are_c=-incomparable by Def8; then not Int (Cl (A `)) c= Cl (Int (A `)) by XBOOLE_0:def_9; then A5: not Int (Cl A) c= Cl (Int A) by A2, A1, SUBSET_1:12; not Cl (Int (A `)) c= Int (Cl (A `)) by A4, XBOOLE_0:def_9; then not Cl (Int A) c= Int (Cl A) by A2, A1, SUBSET_1:12; then Cl (Int A), Int (Cl A) are_c=-incomparable by A5, XBOOLE_0:def_9; hence A is 3rd_class by Def8; ::_thesis: verum end; ( A is 3rd_class implies A ` is 3rd_class ) proof assume A is 3rd_class ; ::_thesis: A ` is 3rd_class then A6: Cl (Int A), Int (Cl A) are_c=-incomparable by Def8; then not Int (Cl A) c= Cl (Int A) by XBOOLE_0:def_9; then A7: not Int (Cl (A `)) c= Cl (Int (A `)) by A2, A1, SUBSET_1:12; not Cl (Int A) c= Int (Cl A) by A6, XBOOLE_0:def_9; then not Cl (Int (A `)) c= Int (Cl (A `)) by A2, A1, SUBSET_1:12; then Cl (Int (A `)), Int (Cl (A `)) are_c=-incomparable by A7, XBOOLE_0:def_9; hence A ` is 3rd_class by Def8; ::_thesis: verum end; hence ( A is 3rd_class iff A ` is 3rd_class ) by A3; ::_thesis: verum end; registration let T be TopSpace; let A be 1st_class Subset of T; clusterA ` -> 1st_class ; coherence A ` is 1st_class by Th38; end; registration let T be with_2nd_class_subsets TopSpace; let A be 2nd_class Subset of T; clusterA ` -> 2nd_class ; coherence A ` is 2nd_class by Th39; end; registration let T be with_3rd_class_subsets TopSpace; let A be 3rd_class Subset of T; clusterA ` -> 3rd_class ; coherence A ` is 3rd_class by Th40; end; theorem Th41: :: ISOMICHI:41 for T being TopSpace for A being Subset of T st A is 1st_class holds ( Int (Cl A) = Int (Cl (Int A)) & Cl (Int A) = Cl (Int (Cl A)) ) proof let T be TopSpace; ::_thesis: for A being Subset of T st A is 1st_class holds ( Int (Cl A) = Int (Cl (Int A)) & Cl (Int A) = Cl (Int (Cl A)) ) let A be Subset of T; ::_thesis: ( A is 1st_class implies ( Int (Cl A) = Int (Cl (Int A)) & Cl (Int A) = Cl (Int (Cl A)) ) ) Cl (Int A) c= Cl A by PRE_TOPC:19, TOPS_1:16; then A1: Int (Cl (Int A)) c= Int (Cl A) by TOPS_1:19; Int A c= Int (Cl A) by PRE_TOPC:18, TOPS_1:19; then A2: Cl (Int A) c= Cl (Int (Cl A)) by PRE_TOPC:19; assume A is 1st_class ; ::_thesis: ( Int (Cl A) = Int (Cl (Int A)) & Cl (Int A) = Cl (Int (Cl A)) ) then A3: Int (Cl A) c= Cl (Int A) by Def6; then A4: Cl (Int (Cl A)) c= Cl (Cl (Int A)) by PRE_TOPC:19; Int (Int (Cl A)) c= Int (Cl (Int A)) by A3, TOPS_1:19; hence ( Int (Cl A) = Int (Cl (Int A)) & Cl (Int A) = Cl (Int (Cl A)) ) by A1, A4, A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th42: :: ISOMICHI:42 for T being TopSpace for A being Subset of T st ( Int (Cl A) = Int (Cl (Int A)) or Cl (Int A) = Cl (Int (Cl A)) ) holds A is 1st_class proof let T be TopSpace; ::_thesis: for A being Subset of T st ( Int (Cl A) = Int (Cl (Int A)) or Cl (Int A) = Cl (Int (Cl A)) ) holds A is 1st_class let A be Subset of T; ::_thesis: ( ( Int (Cl A) = Int (Cl (Int A)) or Cl (Int A) = Cl (Int (Cl A)) ) implies A is 1st_class ) assume A1: ( Int (Cl A) = Int (Cl (Int A)) or Cl (Int A) = Cl (Int (Cl A)) ) ; ::_thesis: A is 1st_class percases ( Int (Cl A) = Int (Cl (Int A)) or Cl (Int A) = Cl (Int (Cl A)) ) by A1; supposeA2: Int (Cl A) = Int (Cl (Int A)) ; ::_thesis: A is 1st_class Int (Cl (Int A)) c= Cl (Int A) by TOPS_1:16; hence A is 1st_class by A2, Def6; ::_thesis: verum end; supposeA3: Cl (Int A) = Cl (Int (Cl A)) ; ::_thesis: A is 1st_class Int (Cl A) c= Cl (Int (Cl A)) by PRE_TOPC:18; hence A is 1st_class by A3, Def6; ::_thesis: verum end; end; end; theorem Th43: :: ISOMICHI:43 for T being TopSpace for A, B being Subset of T st A is 1st_class & B is 1st_class holds ( (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) & (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) ) proof let T be TopSpace; ::_thesis: for A, B being Subset of T st A is 1st_class & B is 1st_class holds ( (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) & (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) ) let A, B be Subset of T; ::_thesis: ( A is 1st_class & B is 1st_class implies ( (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) & (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) ) ) assume that A1: A is 1st_class and A2: B is 1st_class ; ::_thesis: ( (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) & (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) ) A3: Cl (Int B) = Cl (Int (Cl B)) by A2, Th41; Cl (Int A) = Cl (Int (Cl A)) by A1, Th41; then A4: (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (Cl (A \/ B))) by A3, Th2; Int (Cl (A /\ B)) c= Int ((Cl A) /\ (Cl B)) by PRE_TOPC:21, TOPS_1:19; then A5: Int (Cl (A /\ B)) c= (Int (Cl A)) /\ (Int (Cl B)) by TOPS_1:17; Int (A \/ B) c= Int (Cl (A \/ B)) by PRE_TOPC:18, TOPS_1:19; then A6: Cl (Int (A \/ B)) c= Cl (Int (Cl (A \/ B))) by PRE_TOPC:19; Cl ((Int A) \/ (Int B)) c= Cl (Int (A \/ B)) by PRE_TOPC:19, TOPS_1:20; then A7: (Cl (Int A)) \/ (Cl (Int B)) c= Cl (Int (A \/ B)) by PRE_TOPC:20; A8: Int (Cl B) = Int (Cl (Int B)) by A2, Th41; Cl (Int (A /\ B)) c= Cl (A /\ B) by PRE_TOPC:19, TOPS_1:16; then A9: Int (Cl (Int (A /\ B))) c= Int (Cl (A /\ B)) by TOPS_1:19; Int (Cl A) = Int (Cl (Int A)) by A1, Th41; then (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (Int (A /\ B))) by A8, Th1; hence ( (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) & (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) ) by A5, A9, A7, A4, A6, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: ISOMICHI:44 for T being TopSpace for A, B being Subset of T st A is 1st_class & B is 1st_class holds ( A \/ B is 1st_class & A /\ B is 1st_class ) proof let T be TopSpace; ::_thesis: for A, B being Subset of T st A is 1st_class & B is 1st_class holds ( A \/ B is 1st_class & A /\ B is 1st_class ) let A, B be Subset of T; ::_thesis: ( A is 1st_class & B is 1st_class implies ( A \/ B is 1st_class & A /\ B is 1st_class ) ) assume that A1: A is 1st_class and A2: B is 1st_class ; ::_thesis: ( A \/ B is 1st_class & A /\ B is 1st_class ) A3: Cl (Int A) = Cl (Int (Cl A)) by A1, Th41; A4: Int (Cl B) = Int (Cl (Int B)) by A2, Th41; A5: Int (Cl A) = Int (Cl (Int A)) by A1, Th41; A6: Cl (Int B) = Cl (Int (Cl B)) by A2, Th41; A7: Cl (Int (A \/ B)) = (Cl (Int A)) \/ (Cl (Int B)) by A1, A2, Th43 .= Cl (Int (Cl (A \/ B))) by A3, A6, Th2 ; Int (Cl (A /\ B)) = (Int (Cl A)) /\ (Int (Cl B)) by A1, A2, Th43 .= Int (Cl (Int (A /\ B))) by A5, A4, Th1 ; hence ( A \/ B is 1st_class & A /\ B is 1st_class ) by A7, Th42; ::_thesis: verum end;