:: TEX_4 semantic presentation begin registration let X be non empty TopSpace; let A be non empty Subset of X; cluster Cl A -> non empty ; coherence not Cl A is empty by PCOMPS_1:2; end; registration let X be TopSpace; let A be empty Subset of X; cluster Cl A -> empty ; coherence Cl A is empty by PRE_TOPC:22; end; registration let X be non empty TopSpace; let A be non proper Subset of X; cluster Cl A -> non proper ; coherence not Cl A is proper proof A = [#] X by SUBSET_1:def_6; hence not Cl A is proper by TOPS_1:2; ::_thesis: verum end; end; registration let X be non trivial TopSpace; let A be non trivial Subset of X; cluster Cl A -> non trivial ; coherence not Cl A is trivial proof A c= Cl A by PRE_TOPC:18; hence not Cl A is trivial ; ::_thesis: verum end; end; theorem Th1: :: TEX_4:1 for X being non empty TopSpace for A being Subset of X holds Cl A = meet { F where F is Subset of X : ( F is closed & A c= F ) } proof let X be non empty TopSpace; ::_thesis: for A being Subset of X holds Cl A = meet { F where F is Subset of X : ( F is closed & A c= F ) } let A be Subset of X; ::_thesis: Cl A = meet { F where F is Subset of X : ( F is closed & A c= F ) } set G = { F where F is Subset of X : ( F is closed & A c= F ) } ; A1: { F where F is Subset of X : ( F is closed & A c= F ) } c= bool the carrier of X proof let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { F where F is Subset of X : ( F is closed & A c= F ) } or C in bool the carrier of X ) assume C in { F where F is Subset of X : ( F is closed & A c= F ) } ; ::_thesis: C in bool the carrier of X then ex P being Subset of X st ( C = P & P is closed & A c= P ) ; hence C in bool the carrier of X ; ::_thesis: verum end; [#] X in { F where F is Subset of X : ( F is closed & A c= F ) } ; then reconsider G = { F where F is Subset of X : ( F is closed & A c= F ) } as non empty Subset-Family of X by A1; now__::_thesis:_for_P_being_set_st_P_in_G_holds_ A_c=_P let P be set ; ::_thesis: ( P in G implies A c= P ) assume P in G ; ::_thesis: A c= P then ex F being Subset of X st ( F = P & F is closed & A c= F ) ; hence A c= P ; ::_thesis: verum end; then A2: A c= meet G by SETFAM_1:5; A c= Cl A by PRE_TOPC:18; then Cl A in G ; then A3: meet G c= Cl A by SETFAM_1:3; now__::_thesis:_for_S_being_Subset_of_X_st_S_in_G_holds_ S_is_closed let S be Subset of X; ::_thesis: ( S in G implies S is closed ) assume S in G ; ::_thesis: S is closed then ex F being Subset of X st ( F = S & F is closed & A c= F ) ; hence S is closed ; ::_thesis: verum end; then G is closed by TOPS_2:def_2; then Cl A c= meet G by A2, TOPS_1:5, TOPS_2:22; hence Cl A = meet { F where F is Subset of X : ( F is closed & A c= F ) } by A3, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th2: :: TEX_4:2 for X being non empty TopSpace for x being Point of X holds Cl {x} = meet { F where F is Subset of X : ( F is closed & x in F ) } proof let X be non empty TopSpace; ::_thesis: for x being Point of X holds Cl {x} = meet { F where F is Subset of X : ( F is closed & x in F ) } let x be Point of X; ::_thesis: Cl {x} = meet { F where F is Subset of X : ( F is closed & x in F ) } set G = { F where F is Subset of X : ( F is closed & x in F ) } ; set H = { F where F is Subset of X : ( F is closed & {x} c= F ) } ; now__::_thesis:_for_P_being_set_st_P_in__{__F_where_F_is_Subset_of_X_:_(_F_is_closed_&_x_in_F_)__}__holds_ P_in__{__F_where_F_is_Subset_of_X_:_(_F_is_closed_&_{x}_c=_F_)__}_ let P be set ; ::_thesis: ( P in { F where F is Subset of X : ( F is closed & x in F ) } implies P in { F where F is Subset of X : ( F is closed & {x} c= F ) } ) assume P in { F where F is Subset of X : ( F is closed & x in F ) } ; ::_thesis: P in { F where F is Subset of X : ( F is closed & {x} c= F ) } then consider F being Subset of X such that A1: F = P and A2: F is closed and A3: x in F ; {x} c= F by A3, ZFMISC_1:31; hence P in { F where F is Subset of X : ( F is closed & {x} c= F ) } by A1, A2; ::_thesis: verum end; then A4: { F where F is Subset of X : ( F is closed & x in F ) } c= { F where F is Subset of X : ( F is closed & {x} c= F ) } by TARSKI:def_3; now__::_thesis:_for_P_being_set_st_P_in__{__F_where_F_is_Subset_of_X_:_(_F_is_closed_&_{x}_c=_F_)__}__holds_ P_in__{__F_where_F_is_Subset_of_X_:_(_F_is_closed_&_x_in_F_)__}_ let P be set ; ::_thesis: ( P in { F where F is Subset of X : ( F is closed & {x} c= F ) } implies P in { F where F is Subset of X : ( F is closed & x in F ) } ) assume P in { F where F is Subset of X : ( F is closed & {x} c= F ) } ; ::_thesis: P in { F where F is Subset of X : ( F is closed & x in F ) } then consider F being Subset of X such that A5: F = P and A6: F is closed and A7: {x} c= F ; x in F by A7, ZFMISC_1:31; hence P in { F where F is Subset of X : ( F is closed & x in F ) } by A5, A6; ::_thesis: verum end; then A8: { F where F is Subset of X : ( F is closed & {x} c= F ) } c= { F where F is Subset of X : ( F is closed & x in F ) } by TARSKI:def_3; Cl {x} = meet { F where F is Subset of X : ( F is closed & {x} c= F ) } by Th1; hence Cl {x} = meet { F where F is Subset of X : ( F is closed & x in F ) } by A4, A8, XBOOLE_0:def_10; ::_thesis: verum end; registration let X be non empty TopSpace; let A be non proper Subset of X; cluster Int A -> non proper ; coherence not Int A is proper proof A = [#] X by SUBSET_1:def_6; hence not Int A is proper by TOPS_1:15; ::_thesis: verum end; end; registration let X be non empty TopSpace; let A be proper Subset of X; cluster Int A -> proper ; coherence Int A is proper proof now__::_thesis:_Int_A_is_proper assume not Int A is proper ; ::_thesis: contradiction then A1: Int A = [#] X by SUBSET_1:def_6; Int A c= A by TOPS_1:16; hence contradiction by A1, XBOOLE_0:def_10; ::_thesis: verum end; hence Int A is proper ; ::_thesis: verum end; end; registration let X be non empty TopSpace; let A be empty Subset of X; cluster Int A -> empty ; coherence Int A is empty ; end; theorem :: TEX_4:3 for X being non empty TopSpace for A being Subset of X holds Int A = union { G where G is Subset of X : ( G is open & G c= A ) } proof let X be non empty TopSpace; ::_thesis: for A being Subset of X holds Int A = union { G where G is Subset of X : ( G is open & G c= A ) } let A be Subset of X; ::_thesis: Int A = union { G where G is Subset of X : ( G is open & G c= A ) } set F = { G where G is Subset of X : ( G is open & G c= A ) } ; A1: { G where G is Subset of X : ( G is open & G c= A ) } c= bool the carrier of X proof let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { G where G is Subset of X : ( G is open & G c= A ) } or C in bool the carrier of X ) assume C in { G where G is Subset of X : ( G is open & G c= A ) } ; ::_thesis: C in bool the carrier of X then ex P being Subset of X st ( C = P & P is open & P c= A ) ; hence C in bool the carrier of X ; ::_thesis: verum end; {} c= A by XBOOLE_1:2; then {} X in { G where G is Subset of X : ( G is open & G c= A ) } ; then reconsider F = { G where G is Subset of X : ( G is open & G c= A ) } as non empty Subset-Family of X by A1; now__::_thesis:_for_P_being_set_st_P_in_F_holds_ P_c=_A let P be set ; ::_thesis: ( P in F implies P c= A ) assume P in F ; ::_thesis: P c= A then ex G being Subset of X st ( G = P & G is open & G c= A ) ; hence P c= A ; ::_thesis: verum end; then A2: union F c= A by ZFMISC_1:76; Int A c= A by TOPS_1:16; then Int A in F ; then A3: Int A c= union F by ZFMISC_1:74; now__::_thesis:_for_S_being_Subset_of_X_st_S_in_F_holds_ S_is_open let S be Subset of X; ::_thesis: ( S in F implies S is open ) assume S in F ; ::_thesis: S is open then ex G being Subset of X st ( G = S & G is open & G c= A ) ; hence S is open ; ::_thesis: verum end; then F is open by TOPS_2:def_1; then union F c= Int A by A2, TOPS_1:24, TOPS_2:19; hence Int A = union { G where G is Subset of X : ( G is open & G c= A ) } by A3, XBOOLE_0:def_10; ::_thesis: verum end; begin definition let Y be TopStruct ; let IT be Subset of Y; attrIT is anti-discrete means :Def1: :: TEX_4:def 1 for x being Point of Y for G being Subset of Y st G is open & x in G & x in IT holds IT c= G; end; :: deftheorem Def1 defines anti-discrete TEX_4:def_1_:_ for Y being TopStruct for IT being Subset of Y holds ( IT is anti-discrete iff for x being Point of Y for G being Subset of Y st G is open & x in G & x in IT holds IT c= G ); definition let Y be non empty TopStruct ; let A be Subset of Y; redefine attr A is anti-discrete means :Def2: :: TEX_4:def 2 for x being Point of Y for F being Subset of Y st F is closed & x in F & x in A holds A c= F; compatibility ( A is anti-discrete iff for x being Point of Y for F being Subset of Y st F is closed & x in F & x in A holds A c= F ) proof hereby ::_thesis: ( ( for x being Point of Y for F being Subset of Y st F is closed & x in F & x in A holds A c= F ) implies A is anti-discrete ) assume A1: A is anti-discrete ; ::_thesis: for x being Point of Y for F being Subset of Y st F is closed & x in F & x in A holds A c= F let x be Point of Y; ::_thesis: for F being Subset of Y st F is closed & x in F & x in A holds A c= F let F be Subset of Y; ::_thesis: ( F is closed & x in F & x in A implies A c= F ) set G = ([#] Y) \ F; A2: A \ F c= ([#] Y) \ F by XBOOLE_1:33; assume F is closed ; ::_thesis: ( x in F & x in A implies A c= F ) then A3: ([#] Y) \ F is open by PRE_TOPC:def_3; assume A4: x in F ; ::_thesis: ( x in A implies A c= F ) assume A5: x in A ; ::_thesis: A c= F assume not A c= F ; ::_thesis: contradiction then A \ F <> {} by XBOOLE_1:37; then consider a being set such that A6: a in A \ F by XBOOLE_0:def_1; a in A by A6, XBOOLE_0:def_5; then A c= ([#] Y) \ F by A1, A6, A2, A3, Def1; then A7: A misses (([#] Y) \ F) ` by SUBSET_1:24; A8: (([#] Y) \ F) ` = (F `) ` .= F ; not A /\ F is empty by A4, A5, XBOOLE_0:def_4; hence contradiction by A8, A7, XBOOLE_0:def_7; ::_thesis: verum end; hereby ::_thesis: verum assume A9: for x being Point of Y for F being Subset of Y st F is closed & x in F & x in A holds A c= F ; ::_thesis: A is anti-discrete now__::_thesis:_for_x_being_Point_of_Y for_G_being_Subset_of_Y_st_G_is_open_&_x_in_G_&_x_in_A_holds_ A_c=_G let x be Point of Y; ::_thesis: for G being Subset of Y st G is open & x in G & x in A holds A c= G let G be Subset of Y; ::_thesis: ( G is open & x in G & x in A implies A c= G ) set F = ([#] Y) \ G; A10: A \ G c= ([#] Y) \ G by XBOOLE_1:33; A11: G = ([#] Y) \ (([#] Y) \ G) by PRE_TOPC:3; assume G is open ; ::_thesis: ( x in G & x in A implies A c= G ) then A12: ([#] Y) \ G is closed by A11, PRE_TOPC:def_3; assume A13: x in G ; ::_thesis: ( x in A implies A c= G ) assume A14: x in A ; ::_thesis: A c= G assume not A c= G ; ::_thesis: contradiction then A \ G <> {} by XBOOLE_1:37; then consider a being set such that A15: a in A \ G by XBOOLE_0:def_1; A16: ([#] Y) \ G = G ` ; a in A by A15, XBOOLE_0:def_5; then A c= ([#] Y) \ G by A9, A15, A10, A12; then A misses (([#] Y) \ G) ` by SUBSET_1:24; hence contradiction by A13, A14, A16, XBOOLE_0:3; ::_thesis: verum end; hence A is anti-discrete by Def1; ::_thesis: verum end; end; end; :: deftheorem Def2 defines anti-discrete TEX_4:def_2_:_ for Y being non empty TopStruct for A being Subset of Y holds ( A is anti-discrete iff for x being Point of Y for F being Subset of Y st F is closed & x in F & x in A holds A c= F ); definition let Y be TopStruct ; let A be Subset of Y; redefine attr A is anti-discrete means :Def3: :: TEX_4:def 3 for G being Subset of Y holds ( not G is open or A misses G or A c= G ); compatibility ( A is anti-discrete iff for G being Subset of Y holds ( not G is open or A misses G or A c= G ) ) proof hereby ::_thesis: ( ( for G being Subset of Y holds ( not G is open or A misses G or A c= G ) ) implies A is anti-discrete ) assume A1: A is anti-discrete ; ::_thesis: for G being Subset of Y st G is open & A meets G holds A c= G let G be Subset of Y; ::_thesis: ( G is open & A meets G implies A c= G ) assume A2: G is open ; ::_thesis: ( A meets G implies A c= G ) assume A meets G ; ::_thesis: A c= G then consider a being set such that A3: a in A /\ G by XBOOLE_0:4; reconsider a = a as Point of Y by A3; A4: a in G by A3, XBOOLE_0:def_4; a in A by A3, XBOOLE_0:def_4; hence A c= G by A1, A2, A4, Def1; ::_thesis: verum end; assume A5: for G being Subset of Y holds ( not G is open or A misses G or A c= G ) ; ::_thesis: A is anti-discrete now__::_thesis:_for_x_being_Point_of_Y for_G_being_Subset_of_Y_st_G_is_open_&_x_in_G_&_x_in_A_holds_ A_c=_G let x be Point of Y; ::_thesis: for G being Subset of Y st G is open & x in G & x in A holds A c= G let G be Subset of Y; ::_thesis: ( G is open & x in G & x in A implies A c= G ) assume A6: G is open ; ::_thesis: ( x in G & x in A implies A c= G ) assume A7: x in G ; ::_thesis: ( x in A implies A c= G ) assume x in A ; ::_thesis: A c= G then A meets G by A7, XBOOLE_0:3; hence A c= G by A5, A6; ::_thesis: verum end; hence A is anti-discrete by Def1; ::_thesis: verum end; end; :: deftheorem Def3 defines anti-discrete TEX_4:def_3_:_ for Y being TopStruct for A being Subset of Y holds ( A is anti-discrete iff for G being Subset of Y holds ( not G is open or A misses G or A c= G ) ); definition let Y be TopStruct ; let A be Subset of Y; redefine attr A is anti-discrete means :Def4: :: TEX_4:def 4 for F being Subset of Y holds ( not F is closed or A misses F or A c= F ); compatibility ( A is anti-discrete iff for F being Subset of Y holds ( not F is closed or A misses F or A c= F ) ) proof hereby ::_thesis: ( ( for F being Subset of Y holds ( not F is closed or A misses F or A c= F ) ) implies A is anti-discrete ) assume A1: A is anti-discrete ; ::_thesis: for G being Subset of Y st G is closed & A meets G holds A c= G let G be Subset of Y; ::_thesis: ( G is closed & A meets G implies A c= G ) assume G is closed ; ::_thesis: ( A meets G implies A c= G ) then ([#] Y) \ G is open by PRE_TOPC:def_3; then A2: ( A misses G ` or A c= G ` ) by A1, Def3; assume A meets G ; ::_thesis: A c= G then A c= (G `) ` by A2, SUBSET_1:23; hence A c= G ; ::_thesis: verum end; hereby ::_thesis: verum assume A3: for G being Subset of Y holds ( not G is closed or A misses G or A c= G ) ; ::_thesis: A is anti-discrete now__::_thesis:_for_G_being_Subset_of_Y_st_G_is_open_&_A_meets_G_holds_ A_c=_G let G be Subset of Y; ::_thesis: ( G is open & A meets G implies A c= G ) A4: G = ([#] Y) \ (([#] Y) \ G) by PRE_TOPC:3; assume G is open ; ::_thesis: ( A meets G implies A c= G ) then ([#] Y) \ G is closed by A4, PRE_TOPC:def_3; then A5: ( A misses G ` or A c= G ` ) by A3; assume A meets G ; ::_thesis: A c= G then A c= (G `) ` by A5, SUBSET_1:23; hence A c= G ; ::_thesis: verum end; hence A is anti-discrete by Def3; ::_thesis: verum end; end; end; :: deftheorem Def4 defines anti-discrete TEX_4:def_4_:_ for Y being TopStruct for A being Subset of Y holds ( A is anti-discrete iff for F being Subset of Y holds ( not F is closed or A misses F or A c= F ) ); theorem Th4: :: TEX_4:4 for Y0, Y1 being TopStruct for D0 being Subset of Y0 for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is anti-discrete holds D1 is anti-discrete proof let Y0, Y1 be TopStruct ; ::_thesis: for D0 being Subset of Y0 for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is anti-discrete holds D1 is anti-discrete let D0 be Subset of Y0; ::_thesis: for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is anti-discrete holds D1 is anti-discrete let D1 be Subset of Y1; ::_thesis: ( TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is anti-discrete implies D1 is anti-discrete ) assume A1: TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) ; ::_thesis: ( not D0 = D1 or not D0 is anti-discrete or D1 is anti-discrete ) assume A2: D0 = D1 ; ::_thesis: ( not D0 is anti-discrete or D1 is anti-discrete ) assume A3: D0 is anti-discrete ; ::_thesis: D1 is anti-discrete now__::_thesis:_for_D_being_Subset_of_Y1_holds_ (_not_D_is_open_or_D1_misses_D_or_D1_c=_D_) let D be Subset of Y1; ::_thesis: ( not D is open or D1 misses D or D1 c= D ) reconsider E = D as Subset of Y0 by A1; assume D is open ; ::_thesis: ( D1 misses D or D1 c= D ) then E in the topology of Y0 by A1, PRE_TOPC:def_2; then E is open by PRE_TOPC:def_2; hence ( D1 misses D or D1 c= D ) by A2, A3, Def3; ::_thesis: verum end; hence D1 is anti-discrete by Def3; ::_thesis: verum end; theorem Th5: :: TEX_4:5 for Y being non empty TopStruct for A, B being Subset of Y st B c= A & A is anti-discrete holds B is anti-discrete proof let Y be non empty TopStruct ; ::_thesis: for A, B being Subset of Y st B c= A & A is anti-discrete holds B is anti-discrete let A, B be Subset of Y; ::_thesis: ( B c= A & A is anti-discrete implies B is anti-discrete ) assume A1: B c= A ; ::_thesis: ( not A is anti-discrete or B is anti-discrete ) assume A2: A is anti-discrete ; ::_thesis: B is anti-discrete now__::_thesis:_for_G_being_Subset_of_Y_st_G_is_open_&_B_meets_G_holds_ B_c=_G let G be Subset of Y; ::_thesis: ( G is open & B meets G implies B c= G ) assume A3: G is open ; ::_thesis: ( B meets G implies B c= G ) assume B meets G ; ::_thesis: B c= G then B /\ G <> {} by XBOOLE_0:def_7; then A /\ G <> {} by A1, XBOOLE_1:3, XBOOLE_1:26; then A meets G by XBOOLE_0:def_7; then A c= G by A2, A3, Def3; hence B c= G by A1, XBOOLE_1:1; ::_thesis: verum end; hence B is anti-discrete by Def3; ::_thesis: verum end; theorem Th6: :: TEX_4:6 for Y being non empty TopStruct for x being Point of Y holds {x} is anti-discrete proof let Y be non empty TopStruct ; ::_thesis: for x being Point of Y holds {x} is anti-discrete let x be Point of Y; ::_thesis: {x} is anti-discrete now__::_thesis:_for_G_being_Subset_of_Y_st_G_is_open_&_{x}_meets_G_holds_ {x}_c=_G let G be Subset of Y; ::_thesis: ( G is open & {x} meets G implies {x} c= G ) assume G is open ; ::_thesis: ( {x} meets G implies {x} c= G ) assume {x} meets G ; ::_thesis: {x} c= G then consider a being set such that A1: a in {x} /\ G by XBOOLE_0:4; a in {x} by A1, XBOOLE_0:def_4; then A2: a = x by TARSKI:def_1; a in G by A1, XBOOLE_0:def_4; hence {x} c= G by A2, ZFMISC_1:31; ::_thesis: verum end; hence {x} is anti-discrete by Def3; ::_thesis: verum end; theorem Th7: :: TEX_4:7 for Y being non empty TopStruct for A being empty Subset of Y holds A is anti-discrete proof let Y be non empty TopStruct ; ::_thesis: for A being empty Subset of Y holds A is anti-discrete let A be empty Subset of Y; ::_thesis: A is anti-discrete for G being Subset of Y holds ( not G is open or A misses G or A c= G ) by XBOOLE_1:65; hence A is anti-discrete by Def3; ::_thesis: verum end; definition let Y be TopStruct ; let IT be Subset-Family of Y; attrIT is anti-discrete-set-family means :Def5: :: TEX_4:def 5 for A being Subset of Y st A in IT holds A is anti-discrete ; end; :: deftheorem Def5 defines anti-discrete-set-family TEX_4:def_5_:_ for Y being TopStruct for IT being Subset-Family of Y holds ( IT is anti-discrete-set-family iff for A being Subset of Y st A in IT holds A is anti-discrete ); theorem Th8: :: TEX_4:8 for Y being non empty TopStruct for F being Subset-Family of Y st F is anti-discrete-set-family & meet F <> {} holds union F is anti-discrete proof let Y be non empty TopStruct ; ::_thesis: for F being Subset-Family of Y st F is anti-discrete-set-family & meet F <> {} holds union F is anti-discrete let F be Subset-Family of Y; ::_thesis: ( F is anti-discrete-set-family & meet F <> {} implies union F is anti-discrete ) assume A1: F is anti-discrete-set-family ; ::_thesis: ( not meet F <> {} or union F is anti-discrete ) assume A2: meet F <> {} ; ::_thesis: union F is anti-discrete for G being Subset of Y holds ( not G is open or union F misses G or union F c= G ) proof let G be Subset of Y; ::_thesis: ( not G is open or union F misses G or union F c= G ) assume A3: G is open ; ::_thesis: ( union F misses G or union F c= G ) assume union F meets G ; ::_thesis: union F c= G then consider A0 being set such that A4: A0 in F and A5: A0 meets G by ZFMISC_1:80; reconsider A0 = A0 as Subset of Y by A4; A0 is anti-discrete by A1, A4, Def5; then A6: A0 c= G by A3, A5, Def3; meet F c= A0 by A4, SETFAM_1:3; then A7: meet F c= G by A6, XBOOLE_1:1; for B being set st B in F holds B c= G proof let B be set ; ::_thesis: ( B in F implies B c= G ) assume A8: B in F ; ::_thesis: B c= G then reconsider B0 = B as Subset of Y ; meet F c= B0 by A8, SETFAM_1:3; then B0 /\ G <> {} by A2, A7, XBOOLE_1:3, XBOOLE_1:19; then A9: B0 meets G by XBOOLE_0:def_7; B0 is anti-discrete by A1, A8, Def5; hence B c= G by A3, A9, Def3; ::_thesis: verum end; hence union F c= G by ZFMISC_1:76; ::_thesis: verum end; hence union F is anti-discrete by Def3; ::_thesis: verum end; theorem :: TEX_4:9 for Y being non empty TopStruct for F being Subset-Family of Y st F is anti-discrete-set-family holds meet F is anti-discrete proof let Y be non empty TopStruct ; ::_thesis: for F being Subset-Family of Y st F is anti-discrete-set-family holds meet F is anti-discrete let F be Subset-Family of Y; ::_thesis: ( F is anti-discrete-set-family implies meet F is anti-discrete ) assume A1: F is anti-discrete-set-family ; ::_thesis: meet F is anti-discrete hereby ::_thesis: verum percases ( meet F = {} or meet F <> {} ) ; suppose meet F = {} ; ::_thesis: meet F is anti-discrete hence meet F is anti-discrete by Th7; ::_thesis: verum end; supposeA2: meet F <> {} ; ::_thesis: meet F is anti-discrete meet F c= union F by SETFAM_1:2; hence meet F is anti-discrete by A1, A2, Th5, Th8; ::_thesis: verum end; end; end; end; definition let Y be TopStruct ; let x be Point of Y; func MaxADSF x -> Subset-Family of Y equals :: TEX_4:def 6 { A where A is Subset of Y : ( A is anti-discrete & x in A ) } ; coherence { A where A is Subset of Y : ( A is anti-discrete & x in A ) } is Subset-Family of Y proof set F = { A where A is Subset of Y : ( A is anti-discrete & x in A ) } ; { A where A is Subset of Y : ( A is anti-discrete & x in A ) } c= bool the carrier of Y proof let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { A where A is Subset of Y : ( A is anti-discrete & x in A ) } or C in bool the carrier of Y ) assume C in { A where A is Subset of Y : ( A is anti-discrete & x in A ) } ; ::_thesis: C in bool the carrier of Y then ex A being Subset of Y st ( C = A & A is anti-discrete & x in A ) ; hence C in bool the carrier of Y ; ::_thesis: verum end; hence { A where A is Subset of Y : ( A is anti-discrete & x in A ) } is Subset-Family of Y ; ::_thesis: verum end; end; :: deftheorem defines MaxADSF TEX_4:def_6_:_ for Y being TopStruct for x being Point of Y holds MaxADSF x = { A where A is Subset of Y : ( A is anti-discrete & x in A ) } ; registration let Y be non empty TopStruct ; let x be Point of Y; cluster MaxADSF x -> non empty ; coherence not MaxADSF x is empty proof set F = { A where A is Subset of Y : ( A is anti-discrete & x in A ) } ; A1: x in {x} by TARSKI:def_1; {x} is anti-discrete by Th6; then {x} in { A where A is Subset of Y : ( A is anti-discrete & x in A ) } by A1; hence not MaxADSF x is empty ; ::_thesis: verum end; end; theorem Th10: :: TEX_4:10 for Y being non empty TopStruct for x being Point of Y holds MaxADSF x is anti-discrete-set-family proof let Y be non empty TopStruct ; ::_thesis: for x being Point of Y holds MaxADSF x is anti-discrete-set-family let x be Point of Y; ::_thesis: MaxADSF x is anti-discrete-set-family now__::_thesis:_for_A_being_Subset_of_Y_st_A_in_MaxADSF_x_holds_ A_is_anti-discrete let A be Subset of Y; ::_thesis: ( A in MaxADSF x implies A is anti-discrete ) assume A in MaxADSF x ; ::_thesis: A is anti-discrete then ex C being Subset of Y st ( C = A & C is anti-discrete & x in C ) ; hence A is anti-discrete ; ::_thesis: verum end; hence MaxADSF x is anti-discrete-set-family by Def5; ::_thesis: verum end; theorem Th11: :: TEX_4:11 for Y being non empty TopStruct for x being Point of Y holds {x} = meet (MaxADSF x) proof let Y be non empty TopStruct ; ::_thesis: for x being Point of Y holds {x} = meet (MaxADSF x) let x be Point of Y; ::_thesis: {x} = meet (MaxADSF x) A1: x in {x} by TARSKI:def_1; now__::_thesis:_for_A_being_set_st_A_in_MaxADSF_x_holds_ {x}_c=_A let A be set ; ::_thesis: ( A in MaxADSF x implies {x} c= A ) assume A in MaxADSF x ; ::_thesis: {x} c= A then ex C being Subset of Y st ( C = A & C is anti-discrete & x in C ) ; hence {x} c= A by ZFMISC_1:31; ::_thesis: verum end; then A2: {x} c= meet (MaxADSF x) by SETFAM_1:5; {x} is anti-discrete by Th6; then {x} in MaxADSF x by A1; then meet (MaxADSF x) c= {x} by SETFAM_1:3; hence {x} = meet (MaxADSF x) by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th12: :: TEX_4:12 for Y being non empty TopStruct for x being Point of Y holds {x} c= union (MaxADSF x) proof let Y be non empty TopStruct ; ::_thesis: for x being Point of Y holds {x} c= union (MaxADSF x) let x be Point of Y; ::_thesis: {x} c= union (MaxADSF x) {x} = meet (MaxADSF x) by Th11; hence {x} c= union (MaxADSF x) by SETFAM_1:2; ::_thesis: verum end; theorem Th13: :: TEX_4:13 for Y being non empty TopStruct for x being Point of Y holds union (MaxADSF x) is anti-discrete proof let Y be non empty TopStruct ; ::_thesis: for x being Point of Y holds union (MaxADSF x) is anti-discrete let x be Point of Y; ::_thesis: union (MaxADSF x) is anti-discrete {x} = meet (MaxADSF x) by Th11; hence union (MaxADSF x) is anti-discrete by Th8, Th10; ::_thesis: verum end; begin definition let Y be TopStruct ; let IT be Subset of Y; attrIT is maximal_anti-discrete means :Def7: :: TEX_4:def 7 ( IT is anti-discrete & ( for D being Subset of Y st D is anti-discrete & IT c= D holds IT = D ) ); end; :: deftheorem Def7 defines maximal_anti-discrete TEX_4:def_7_:_ for Y being TopStruct for IT being Subset of Y holds ( IT is maximal_anti-discrete iff ( IT is anti-discrete & ( for D being Subset of Y st D is anti-discrete & IT c= D holds IT = D ) ) ); theorem :: TEX_4:14 for Y0, Y1 being TopStruct for D0 being Subset of Y0 for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is maximal_anti-discrete holds D1 is maximal_anti-discrete proof let Y0, Y1 be TopStruct ; ::_thesis: for D0 being Subset of Y0 for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is maximal_anti-discrete holds D1 is maximal_anti-discrete let D0 be Subset of Y0; ::_thesis: for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is maximal_anti-discrete holds D1 is maximal_anti-discrete let D1 be Subset of Y1; ::_thesis: ( TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is maximal_anti-discrete implies D1 is maximal_anti-discrete ) assume A1: TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) ; ::_thesis: ( not D0 = D1 or not D0 is maximal_anti-discrete or D1 is maximal_anti-discrete ) assume A2: D0 = D1 ; ::_thesis: ( not D0 is maximal_anti-discrete or D1 is maximal_anti-discrete ) assume A3: D0 is maximal_anti-discrete ; ::_thesis: D1 is maximal_anti-discrete A4: now__::_thesis:_for_D_being_Subset_of_Y1_st_D_is_anti-discrete_&_D1_c=_D_holds_ D1_=_D let D be Subset of Y1; ::_thesis: ( D is anti-discrete & D1 c= D implies D1 = D ) reconsider E = D as Subset of Y0 by A1; assume D is anti-discrete ; ::_thesis: ( D1 c= D implies D1 = D ) then A5: E is anti-discrete by A1, Th4; assume D1 c= D ; ::_thesis: D1 = D hence D1 = D by A2, A3, A5, Def7; ::_thesis: verum end; D0 is anti-discrete by A3, Def7; then D1 is anti-discrete by A1, A2, Th4; hence D1 is maximal_anti-discrete by A4, Def7; ::_thesis: verum end; theorem Th15: :: TEX_4:15 for Y being non empty TopStruct for A being empty Subset of Y holds not A is maximal_anti-discrete proof let Y be non empty TopStruct ; ::_thesis: for A being empty Subset of Y holds not A is maximal_anti-discrete consider a being set such that A1: a in the carrier of Y by XBOOLE_0:def_1; reconsider a = a as Point of Y by A1; let A be empty Subset of Y; ::_thesis: not A is maximal_anti-discrete now__::_thesis:_ex_C_being_Element_of_bool_the_carrier_of_Y_st_ (_C_is_anti-discrete_&_A_c=_C_&_A_<>_C_) take C = {a}; ::_thesis: ( C is anti-discrete & A c= C & A <> C ) thus ( C is anti-discrete & A c= C & A <> C ) by Th6, XBOOLE_1:2; ::_thesis: verum end; hence not A is maximal_anti-discrete by Def7; ::_thesis: verum end; theorem Th16: :: TEX_4:16 for Y being non empty TopStruct for A being non empty Subset of Y st A is anti-discrete & A is open holds A is maximal_anti-discrete proof let Y be non empty TopStruct ; ::_thesis: for A being non empty Subset of Y st A is anti-discrete & A is open holds A is maximal_anti-discrete let A be non empty Subset of Y; ::_thesis: ( A is anti-discrete & A is open implies A is maximal_anti-discrete ) assume A1: A is anti-discrete ; ::_thesis: ( not A is open or A is maximal_anti-discrete ) assume A2: A is open ; ::_thesis: A is maximal_anti-discrete for D being Subset of Y st D is anti-discrete & A c= D holds A = D proof let D be Subset of Y; ::_thesis: ( D is anti-discrete & A c= D implies A = D ) assume D is anti-discrete ; ::_thesis: ( not A c= D or A = D ) then ( D misses A or D c= A ) by A2, Def3; then A3: ( D /\ A = {} or D c= A ) by XBOOLE_0:def_7; assume A c= D ; ::_thesis: A = D hence A = D by A3, XBOOLE_0:def_10, XBOOLE_1:28; ::_thesis: verum end; hence A is maximal_anti-discrete by A1, Def7; ::_thesis: verum end; theorem Th17: :: TEX_4:17 for Y being non empty TopStruct for A being non empty Subset of Y st A is anti-discrete & A is closed holds A is maximal_anti-discrete proof let Y be non empty TopStruct ; ::_thesis: for A being non empty Subset of Y st A is anti-discrete & A is closed holds A is maximal_anti-discrete let A be non empty Subset of Y; ::_thesis: ( A is anti-discrete & A is closed implies A is maximal_anti-discrete ) assume A1: A is anti-discrete ; ::_thesis: ( not A is closed or A is maximal_anti-discrete ) assume A2: A is closed ; ::_thesis: A is maximal_anti-discrete for D being Subset of Y st D is anti-discrete & A c= D holds A = D proof let D be Subset of Y; ::_thesis: ( D is anti-discrete & A c= D implies A = D ) assume D is anti-discrete ; ::_thesis: ( not A c= D or A = D ) then ( D misses A or D c= A ) by A2, Def4; then A3: ( D /\ A = {} or D c= A ) by XBOOLE_0:def_7; assume A c= D ; ::_thesis: A = D hence A = D by A3, XBOOLE_0:def_10, XBOOLE_1:28; ::_thesis: verum end; hence A is maximal_anti-discrete by A1, Def7; ::_thesis: verum end; definition let Y be TopStruct ; let x be Point of Y; func MaxADSet x -> Subset of Y equals :: TEX_4:def 8 union (MaxADSF x); coherence union (MaxADSF x) is Subset of Y ; end; :: deftheorem defines MaxADSet TEX_4:def_8_:_ for Y being TopStruct for x being Point of Y holds MaxADSet x = union (MaxADSF x); registration let Y be non empty TopStruct ; let x be Point of Y; cluster MaxADSet x -> non empty ; coherence not MaxADSet x is empty proof {x} c= union (MaxADSF x) by Th12; hence not MaxADSet x is empty ; ::_thesis: verum end; end; theorem :: TEX_4:18 for Y being non empty TopStruct for x being Point of Y holds {x} c= MaxADSet x by Th12; theorem Th19: :: TEX_4:19 for Y being non empty TopStruct for D being Subset of Y for x being Point of Y st D is anti-discrete & x in D holds D c= MaxADSet x proof let Y be non empty TopStruct ; ::_thesis: for D being Subset of Y for x being Point of Y st D is anti-discrete & x in D holds D c= MaxADSet x let D be Subset of Y; ::_thesis: for x being Point of Y st D is anti-discrete & x in D holds D c= MaxADSet x let x be Point of Y; ::_thesis: ( D is anti-discrete & x in D implies D c= MaxADSet x ) assume A1: D is anti-discrete ; ::_thesis: ( not x in D or D c= MaxADSet x ) assume x in D ; ::_thesis: D c= MaxADSet x then D in { A where A is Subset of Y : ( A is anti-discrete & x in A ) } by A1; hence D c= MaxADSet x by ZFMISC_1:74; ::_thesis: verum end; theorem Th20: :: TEX_4:20 for Y being non empty TopStruct for x being Point of Y holds MaxADSet x is maximal_anti-discrete proof let Y be non empty TopStruct ; ::_thesis: for x being Point of Y holds MaxADSet x is maximal_anti-discrete let x be Point of Y; ::_thesis: MaxADSet x is maximal_anti-discrete A1: for D being Subset of Y st D is anti-discrete & MaxADSet x c= D holds MaxADSet x = D proof let D be Subset of Y; ::_thesis: ( D is anti-discrete & MaxADSet x c= D implies MaxADSet x = D ) assume A2: D is anti-discrete ; ::_thesis: ( not MaxADSet x c= D or MaxADSet x = D ) assume A3: MaxADSet x c= D ; ::_thesis: MaxADSet x = D {x} c= MaxADSet x by Th12; then {x} c= D by A3, XBOOLE_1:1; then x in D by ZFMISC_1:31; then D c= MaxADSet x by A2, Th19; hence MaxADSet x = D by A3, XBOOLE_0:def_10; ::_thesis: verum end; MaxADSet x is anti-discrete by Th13; hence MaxADSet x is maximal_anti-discrete by A1, Def7; ::_thesis: verum end; theorem Th21: :: TEX_4:21 for Y being non empty TopStruct for x, y being Point of Y holds ( y in MaxADSet x iff MaxADSet y = MaxADSet x ) proof let Y be non empty TopStruct ; ::_thesis: for x, y being Point of Y holds ( y in MaxADSet x iff MaxADSet y = MaxADSet x ) let x, y be Point of Y; ::_thesis: ( y in MaxADSet x iff MaxADSet y = MaxADSet x ) MaxADSet y is maximal_anti-discrete by Th20; then A1: MaxADSet y is anti-discrete by Def7; A2: MaxADSet x is maximal_anti-discrete by Th20; then A3: MaxADSet x is anti-discrete by Def7; thus ( y in MaxADSet x implies MaxADSet y = MaxADSet x ) ::_thesis: ( MaxADSet y = MaxADSet x implies y in MaxADSet x ) proof assume y in MaxADSet x ; ::_thesis: MaxADSet y = MaxADSet x then MaxADSet x in { A where A is Subset of Y : ( A is anti-discrete & y in A ) } by A3; then MaxADSet x c= MaxADSet y by ZFMISC_1:74; hence MaxADSet y = MaxADSet x by A2, A1, Def7; ::_thesis: verum end; assume A4: MaxADSet y = MaxADSet x ; ::_thesis: y in MaxADSet x {y} c= MaxADSet y by Th12; hence y in MaxADSet x by A4, ZFMISC_1:31; ::_thesis: verum end; theorem Th22: :: TEX_4:22 for Y being non empty TopStruct for x, y being Point of Y holds ( MaxADSet x misses MaxADSet y or MaxADSet x = MaxADSet y ) proof let Y be non empty TopStruct ; ::_thesis: for x, y being Point of Y holds ( MaxADSet x misses MaxADSet y or MaxADSet x = MaxADSet y ) let x, y be Point of Y; ::_thesis: ( MaxADSet x misses MaxADSet y or MaxADSet x = MaxADSet y ) assume (MaxADSet x) /\ (MaxADSet y) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: MaxADSet x = MaxADSet y then consider a being set such that A1: a in (MaxADSet x) /\ (MaxADSet y) by XBOOLE_0:def_1; reconsider a = a as Point of Y by A1; a in MaxADSet x by A1, XBOOLE_0:def_4; then A2: MaxADSet a = MaxADSet x by Th21; a in MaxADSet y by A1, XBOOLE_0:def_4; hence MaxADSet x = MaxADSet y by A2, Th21; ::_thesis: verum end; theorem Th23: :: TEX_4:23 for Y being non empty TopStruct for F being Subset of Y for x being Point of Y st F is closed & x in F holds MaxADSet x c= F proof let Y be non empty TopStruct ; ::_thesis: for F being Subset of Y for x being Point of Y st F is closed & x in F holds MaxADSet x c= F let F be Subset of Y; ::_thesis: for x being Point of Y st F is closed & x in F holds MaxADSet x c= F let x be Point of Y; ::_thesis: ( F is closed & x in F implies MaxADSet x c= F ) assume that A1: F is closed and A2: x in F ; ::_thesis: MaxADSet x c= F {x} c= MaxADSet x by Th12; then A3: x in MaxADSet x by ZFMISC_1:31; MaxADSet x is maximal_anti-discrete by Th20; then MaxADSet x is anti-discrete by Def7; hence MaxADSet x c= F by A1, A2, A3, Def2; ::_thesis: verum end; theorem Th24: :: TEX_4:24 for Y being non empty TopStruct for G being Subset of Y for x being Point of Y st G is open & x in G holds MaxADSet x c= G proof let Y be non empty TopStruct ; ::_thesis: for G being Subset of Y for x being Point of Y st G is open & x in G holds MaxADSet x c= G let G be Subset of Y; ::_thesis: for x being Point of Y st G is open & x in G holds MaxADSet x c= G let x be Point of Y; ::_thesis: ( G is open & x in G implies MaxADSet x c= G ) assume that A1: G is open and A2: x in G ; ::_thesis: MaxADSet x c= G {x} c= MaxADSet x by Th12; then A3: x in MaxADSet x by ZFMISC_1:31; MaxADSet x is maximal_anti-discrete by Th20; then MaxADSet x is anti-discrete by Def7; hence MaxADSet x c= G by A1, A2, A3, Def1; ::_thesis: verum end; theorem :: TEX_4:25 for Y being non empty TopStruct for x being Point of Y holds MaxADSet x c= meet { F where F is Subset of Y : ( F is closed & x in F ) } proof let Y be non empty TopStruct ; ::_thesis: for x being Point of Y holds MaxADSet x c= meet { F where F is Subset of Y : ( F is closed & x in F ) } let x be Point of Y; ::_thesis: MaxADSet x c= meet { F where F is Subset of Y : ( F is closed & x in F ) } set G = { F where F is Subset of Y : ( F is closed & x in F ) } ; { F where F is Subset of Y : ( F is closed & x in F ) } c= bool the carrier of Y proof let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { F where F is Subset of Y : ( F is closed & x in F ) } or C in bool the carrier of Y ) assume C in { F where F is Subset of Y : ( F is closed & x in F ) } ; ::_thesis: C in bool the carrier of Y then ex P being Subset of Y st ( C = P & P is closed & x in P ) ; hence C in bool the carrier of Y ; ::_thesis: verum end; then reconsider G = { F where F is Subset of Y : ( F is closed & x in F ) } as Subset-Family of Y ; now__::_thesis:_for_C_being_set_st_C_in_G_holds_ MaxADSet_x_c=_C let C be set ; ::_thesis: ( C in G implies MaxADSet x c= C ) assume C in G ; ::_thesis: MaxADSet x c= C then ex F being Subset of Y st ( F = C & F is closed & x in F ) ; hence MaxADSet x c= C by Th23; ::_thesis: verum end; hence MaxADSet x c= meet { F where F is Subset of Y : ( F is closed & x in F ) } by SETFAM_1:5; ::_thesis: verum end; theorem :: TEX_4:26 for Y being non empty TopStruct for x being Point of Y holds MaxADSet x c= meet { G where G is Subset of Y : ( G is open & x in G ) } proof let Y be non empty TopStruct ; ::_thesis: for x being Point of Y holds MaxADSet x c= meet { G where G is Subset of Y : ( G is open & x in G ) } let x be Point of Y; ::_thesis: MaxADSet x c= meet { G where G is Subset of Y : ( G is open & x in G ) } set F = { G where G is Subset of Y : ( G is open & x in G ) } ; { G where G is Subset of Y : ( G is open & x in G ) } c= bool the carrier of Y proof let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { G where G is Subset of Y : ( G is open & x in G ) } or C in bool the carrier of Y ) assume C in { G where G is Subset of Y : ( G is open & x in G ) } ; ::_thesis: C in bool the carrier of Y then ex P being Subset of Y st ( C = P & P is open & x in P ) ; hence C in bool the carrier of Y ; ::_thesis: verum end; then reconsider F = { G where G is Subset of Y : ( G is open & x in G ) } as Subset-Family of Y ; now__::_thesis:_for_C_being_set_st_C_in_F_holds_ MaxADSet_x_c=_C let C be set ; ::_thesis: ( C in F implies MaxADSet x c= C ) assume C in F ; ::_thesis: MaxADSet x c= C then ex G being Subset of Y st ( G = C & G is open & x in G ) ; hence MaxADSet x c= C by Th24; ::_thesis: verum end; hence MaxADSet x c= meet { G where G is Subset of Y : ( G is open & x in G ) } by SETFAM_1:5; ::_thesis: verum end; definition let Y be non empty TopStruct ; let A be Subset of Y; redefine attr A is maximal_anti-discrete means :Def9: :: TEX_4:def 9 ex x being Point of Y st ( x in A & A = MaxADSet x ); compatibility ( A is maximal_anti-discrete iff ex x being Point of Y st ( x in A & A = MaxADSet x ) ) proof thus ( A is maximal_anti-discrete implies ex x being Point of Y st ( x in A & A = MaxADSet x ) ) ::_thesis: ( ex x being Point of Y st ( x in A & A = MaxADSet x ) implies A is maximal_anti-discrete ) proof assume A1: A is maximal_anti-discrete ; ::_thesis: ex x being Point of Y st ( x in A & A = MaxADSet x ) then A <> {} by Th15; then consider x being set such that A2: x in A by XBOOLE_0:def_1; reconsider x = x as Point of Y by A2; take x ; ::_thesis: ( x in A & A = MaxADSet x ) thus x in A by A2; ::_thesis: A = MaxADSet x MaxADSet x is maximal_anti-discrete by Th20; then A3: MaxADSet x is anti-discrete by Def7; A is anti-discrete by A1, Def7; then A c= MaxADSet x by A2, Th19; hence A = MaxADSet x by A1, A3, Def7; ::_thesis: verum end; assume ex x being Point of Y st ( x in A & A = MaxADSet x ) ; ::_thesis: A is maximal_anti-discrete hence A is maximal_anti-discrete by Th20; ::_thesis: verum end; end; :: deftheorem Def9 defines maximal_anti-discrete TEX_4:def_9_:_ for Y being non empty TopStruct for A being Subset of Y holds ( A is maximal_anti-discrete iff ex x being Point of Y st ( x in A & A = MaxADSet x ) ); theorem Th27: :: TEX_4:27 for Y being non empty TopStruct for A being Subset of Y for x being Point of Y st x in A & A is maximal_anti-discrete holds A = MaxADSet x proof let Y be non empty TopStruct ; ::_thesis: for A being Subset of Y for x being Point of Y st x in A & A is maximal_anti-discrete holds A = MaxADSet x let A be Subset of Y; ::_thesis: for x being Point of Y st x in A & A is maximal_anti-discrete holds A = MaxADSet x let x be Point of Y; ::_thesis: ( x in A & A is maximal_anti-discrete implies A = MaxADSet x ) assume A1: x in A ; ::_thesis: ( not A is maximal_anti-discrete or A = MaxADSet x ) assume A is maximal_anti-discrete ; ::_thesis: A = MaxADSet x then ex y being Point of Y st ( y in A & A = MaxADSet y ) by Def9; hence A = MaxADSet x by A1, Th21; ::_thesis: verum end; definition let Y be non empty TopStruct ; let A be non empty Subset of Y; redefine attr A is maximal_anti-discrete means :: TEX_4:def 10 for x being Point of Y st x in A holds A = MaxADSet x; compatibility ( A is maximal_anti-discrete iff for x being Point of Y st x in A holds A = MaxADSet x ) proof thus ( A is maximal_anti-discrete implies for x being Point of Y st x in A holds A = MaxADSet x ) by Th27; ::_thesis: ( ( for x being Point of Y st x in A holds A = MaxADSet x ) implies A is maximal_anti-discrete ) consider a being set such that A1: a in A by XBOOLE_0:def_1; reconsider a = a as Point of Y by A1; assume A2: for x being Point of Y st x in A holds A = MaxADSet x ; ::_thesis: A is maximal_anti-discrete now__::_thesis:_ex_a_being_Point_of_Y_st_ (_a_in_A_&_A_=_MaxADSet_a_) take a = a; ::_thesis: ( a in A & A = MaxADSet a ) thus a in A by A1; ::_thesis: A = MaxADSet a thus A = MaxADSet a by A2, A1; ::_thesis: verum end; hence A is maximal_anti-discrete by Def9; ::_thesis: verum end; end; :: deftheorem defines maximal_anti-discrete TEX_4:def_10_:_ for Y being non empty TopStruct for A being non empty Subset of Y holds ( A is maximal_anti-discrete iff for x being Point of Y st x in A holds A = MaxADSet x ); definition let Y be non empty TopStruct ; let A be Subset of Y; func MaxADSet A -> Subset of Y equals :: TEX_4:def 11 union { (MaxADSet a) where a is Point of Y : a in A } ; coherence union { (MaxADSet a) where a is Point of Y : a in A } is Subset of Y proof set M = { (MaxADSet a) where a is Point of Y : a in A } ; { (MaxADSet a) where a is Point of Y : a in A } c= bool the carrier of Y proof let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { (MaxADSet a) where a is Point of Y : a in A } or C in bool the carrier of Y ) assume C in { (MaxADSet a) where a is Point of Y : a in A } ; ::_thesis: C in bool the carrier of Y then ex a being Point of Y st ( C = MaxADSet a & a in A ) ; hence C in bool the carrier of Y ; ::_thesis: verum end; then reconsider M = { (MaxADSet a) where a is Point of Y : a in A } as Subset-Family of Y ; union M is Subset of Y ; hence union { (MaxADSet a) where a is Point of Y : a in A } is Subset of Y ; ::_thesis: verum end; end; :: deftheorem defines MaxADSet TEX_4:def_11_:_ for Y being non empty TopStruct for A being Subset of Y holds MaxADSet A = union { (MaxADSet a) where a is Point of Y : a in A } ; theorem Th28: :: TEX_4:28 for Y being non empty TopStruct for x being Point of Y holds MaxADSet x = MaxADSet {x} proof let Y be non empty TopStruct ; ::_thesis: for x being Point of Y holds MaxADSet x = MaxADSet {x} let x be Point of Y; ::_thesis: MaxADSet x = MaxADSet {x} set M = { (MaxADSet a) where a is Point of Y : a in {x} } ; now__::_thesis:_for_P_being_set_st_P_in__{__(MaxADSet_a)_where_a_is_Point_of_Y_:_a_in_{x}__}__holds_ P_c=_MaxADSet_x let P be set ; ::_thesis: ( P in { (MaxADSet a) where a is Point of Y : a in {x} } implies P c= MaxADSet x ) assume P in { (MaxADSet a) where a is Point of Y : a in {x} } ; ::_thesis: P c= MaxADSet x then ex a being Point of Y st ( P = MaxADSet a & a in {x} ) ; hence P c= MaxADSet x by TARSKI:def_1; ::_thesis: verum end; then A1: MaxADSet {x} c= MaxADSet x by ZFMISC_1:76; x in {x} by TARSKI:def_1; then MaxADSet x in { (MaxADSet a) where a is Point of Y : a in {x} } ; then MaxADSet x c= MaxADSet {x} by ZFMISC_1:74; hence MaxADSet x = MaxADSet {x} by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th29: :: TEX_4:29 for Y being non empty TopStruct for A being Subset of Y for x being Point of Y st MaxADSet x meets MaxADSet A holds MaxADSet x meets A proof let Y be non empty TopStruct ; ::_thesis: for A being Subset of Y for x being Point of Y st MaxADSet x meets MaxADSet A holds MaxADSet x meets A let A be Subset of Y; ::_thesis: for x being Point of Y st MaxADSet x meets MaxADSet A holds MaxADSet x meets A let x be Point of Y; ::_thesis: ( MaxADSet x meets MaxADSet A implies MaxADSet x meets A ) set E = { (MaxADSet a) where a is Point of Y : a in A } ; assume (MaxADSet x) /\ (MaxADSet A) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: MaxADSet x meets A then consider z being set such that A1: z in (MaxADSet x) /\ (MaxADSet A) by XBOOLE_0:def_1; reconsider z = z as Point of Y by A1; z in MaxADSet A by A1, XBOOLE_0:def_4; then consider C being set such that A2: z in C and A3: C in { (MaxADSet a) where a is Point of Y : a in A } by TARSKI:def_4; z in MaxADSet x by A1, XBOOLE_0:def_4; then A4: MaxADSet z = MaxADSet x by Th21; consider b being Point of Y such that A5: C = MaxADSet b and A6: b in A by A3; MaxADSet b = MaxADSet z by A2, A5, Th21; then {b} c= MaxADSet x by A4, Th12; then b in MaxADSet x by ZFMISC_1:31; hence MaxADSet x meets A by A6, XBOOLE_0:3; ::_thesis: verum end; theorem Th30: :: TEX_4:30 for Y being non empty TopStruct for A being Subset of Y for x being Point of Y st MaxADSet x meets MaxADSet A holds MaxADSet x c= MaxADSet A proof let Y be non empty TopStruct ; ::_thesis: for A being Subset of Y for x being Point of Y st MaxADSet x meets MaxADSet A holds MaxADSet x c= MaxADSet A let A be Subset of Y; ::_thesis: for x being Point of Y st MaxADSet x meets MaxADSet A holds MaxADSet x c= MaxADSet A let x be Point of Y; ::_thesis: ( MaxADSet x meets MaxADSet A implies MaxADSet x c= MaxADSet A ) set F = { (MaxADSet b) where b is Point of Y : b in A } ; assume MaxADSet x meets MaxADSet A ; ::_thesis: MaxADSet x c= MaxADSet A then MaxADSet x meets A by Th29; then consider z being set such that A1: z in (MaxADSet x) /\ A by XBOOLE_0:4; reconsider z = z as Point of Y by A1; set E = { (MaxADSet a) where a is Point of Y : a in {z} } ; z in A by A1, XBOOLE_0:def_4; then A2: {z} c= A by ZFMISC_1:31; { (MaxADSet a) where a is Point of Y : a in {z} } c= { (MaxADSet b) where b is Point of Y : b in A } proof let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { (MaxADSet a) where a is Point of Y : a in {z} } or C in { (MaxADSet b) where b is Point of Y : b in A } ) assume C in { (MaxADSet a) where a is Point of Y : a in {z} } ; ::_thesis: C in { (MaxADSet b) where b is Point of Y : b in A } then ex a being Point of Y st ( C = MaxADSet a & a in {z} ) ; hence C in { (MaxADSet b) where b is Point of Y : b in A } by A2; ::_thesis: verum end; then MaxADSet {z} c= MaxADSet A by ZFMISC_1:77; then A3: MaxADSet z c= MaxADSet A by Th28; z in MaxADSet x by A1, XBOOLE_0:def_4; hence MaxADSet x c= MaxADSet A by A3, Th21; ::_thesis: verum end; theorem Th31: :: TEX_4:31 for Y being non empty TopStruct for A, B being Subset of Y st A c= B holds MaxADSet A c= MaxADSet B proof let Y be non empty TopStruct ; ::_thesis: for A, B being Subset of Y st A c= B holds MaxADSet A c= MaxADSet B let A, B be Subset of Y; ::_thesis: ( A c= B implies MaxADSet A c= MaxADSet B ) set E = { (MaxADSet a) where a is Point of Y : a in A } ; set F = { (MaxADSet b) where b is Point of Y : b in B } ; assume A1: A c= B ; ::_thesis: MaxADSet A c= MaxADSet B { (MaxADSet a) where a is Point of Y : a in A } c= { (MaxADSet b) where b is Point of Y : b in B } proof let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { (MaxADSet a) where a is Point of Y : a in A } or C in { (MaxADSet b) where b is Point of Y : b in B } ) assume C in { (MaxADSet a) where a is Point of Y : a in A } ; ::_thesis: C in { (MaxADSet b) where b is Point of Y : b in B } then ex a being Point of Y st ( C = MaxADSet a & a in A ) ; hence C in { (MaxADSet b) where b is Point of Y : b in B } by A1; ::_thesis: verum end; hence MaxADSet A c= MaxADSet B by ZFMISC_1:77; ::_thesis: verum end; theorem Th32: :: TEX_4:32 for Y being non empty TopStruct for A being Subset of Y holds A c= MaxADSet A proof let Y be non empty TopStruct ; ::_thesis: for A being Subset of Y holds A c= MaxADSet A let A be Subset of Y; ::_thesis: A c= MaxADSet A now__::_thesis:_for_x_being_set_st_x_in_A_holds_ x_in_MaxADSet_A let x be set ; ::_thesis: ( x in A implies x in MaxADSet A ) assume A1: x in A ; ::_thesis: x in MaxADSet A then reconsider a = x as Point of Y ; {a} c= A by A1, ZFMISC_1:31; then MaxADSet {a} c= MaxADSet A by Th31; then A2: MaxADSet a c= MaxADSet A by Th28; A3: a in {a} by TARSKI:def_1; {a} c= MaxADSet a by Th12; then {a} c= MaxADSet A by A2, XBOOLE_1:1; hence x in MaxADSet A by A3; ::_thesis: verum end; hence A c= MaxADSet A by TARSKI:def_3; ::_thesis: verum end; theorem Th33: :: TEX_4:33 for Y being non empty TopStruct for A being Subset of Y holds MaxADSet A = MaxADSet (MaxADSet A) proof let Y be non empty TopStruct ; ::_thesis: for A being Subset of Y holds MaxADSet A = MaxADSet (MaxADSet A) let A be Subset of Y; ::_thesis: MaxADSet A = MaxADSet (MaxADSet A) A1: MaxADSet (MaxADSet A) c= MaxADSet A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in MaxADSet (MaxADSet A) or x in MaxADSet A ) assume x in MaxADSet (MaxADSet A) ; ::_thesis: x in MaxADSet A then consider C being set such that A2: x in C and A3: C in { (MaxADSet a) where a is Point of Y : a in MaxADSet A } by TARSKI:def_4; consider a being Point of Y such that A4: C = MaxADSet a and A5: a in MaxADSet A by A3; consider D being set such that A6: a in D and A7: D in { (MaxADSet b) where b is Point of Y : b in A } by A5, TARSKI:def_4; consider b being Point of Y such that A8: D = MaxADSet b and b in A by A7; MaxADSet a = MaxADSet b by A6, A8, Th21; hence x in MaxADSet A by A2, A4, A7, A8, TARSKI:def_4; ::_thesis: verum end; MaxADSet A c= MaxADSet (MaxADSet A) by Th32; hence MaxADSet A = MaxADSet (MaxADSet A) by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th34: :: TEX_4:34 for Y being non empty TopStruct for A, B being Subset of Y st A c= MaxADSet B holds MaxADSet A c= MaxADSet B proof let Y be non empty TopStruct ; ::_thesis: for A, B being Subset of Y st A c= MaxADSet B holds MaxADSet A c= MaxADSet B let A, B be Subset of Y; ::_thesis: ( A c= MaxADSet B implies MaxADSet A c= MaxADSet B ) assume A c= MaxADSet B ; ::_thesis: MaxADSet A c= MaxADSet B then MaxADSet A c= MaxADSet (MaxADSet B) by Th31; hence MaxADSet A c= MaxADSet B by Th33; ::_thesis: verum end; theorem Th35: :: TEX_4:35 for Y being non empty TopStruct for A, B being Subset of Y st B c= MaxADSet A & A c= MaxADSet B holds MaxADSet A = MaxADSet B proof let Y be non empty TopStruct ; ::_thesis: for A, B being Subset of Y st B c= MaxADSet A & A c= MaxADSet B holds MaxADSet A = MaxADSet B let A, B be Subset of Y; ::_thesis: ( B c= MaxADSet A & A c= MaxADSet B implies MaxADSet A = MaxADSet B ) thus ( B c= MaxADSet A & A c= MaxADSet B implies MaxADSet A = MaxADSet B ) ::_thesis: verum proof assume that A1: B c= MaxADSet A and A2: A c= MaxADSet B ; ::_thesis: MaxADSet A = MaxADSet B A3: MaxADSet A c= MaxADSet B by A2, Th34; MaxADSet B c= MaxADSet A by A1, Th34; hence MaxADSet A = MaxADSet B by A3, XBOOLE_0:def_10; ::_thesis: verum end; end; theorem :: TEX_4:36 for Y being non empty TopStruct for A, B being Subset of Y holds MaxADSet (A \/ B) = (MaxADSet A) \/ (MaxADSet B) proof let Y be non empty TopStruct ; ::_thesis: for A, B being Subset of Y holds MaxADSet (A \/ B) = (MaxADSet A) \/ (MaxADSet B) let A, B be Subset of Y; ::_thesis: MaxADSet (A \/ B) = (MaxADSet A) \/ (MaxADSet B) A1: MaxADSet (A \/ B) c= (MaxADSet A) \/ (MaxADSet B) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in MaxADSet (A \/ B) or x in (MaxADSet A) \/ (MaxADSet B) ) assume x in MaxADSet (A \/ B) ; ::_thesis: x in (MaxADSet A) \/ (MaxADSet B) then consider C being set such that A2: x in C and A3: C in { (MaxADSet a) where a is Point of Y : a in A \/ B } by TARSKI:def_4; consider a being Point of Y such that A4: C = MaxADSet a and A5: a in A \/ B by A3; now__::_thesis:_x_in_(MaxADSet_A)_\/_(MaxADSet_B) percases ( a in A or a in B ) by A5, XBOOLE_0:def_3; supposeA6: a in A ; ::_thesis: x in (MaxADSet A) \/ (MaxADSet B) now__::_thesis:_ex_C_being_set_st_ (_x_in_C_&_C_in__{__(MaxADSet_c)_where_c_is_Point_of_Y_:_c_in_A__}__) take C = C; ::_thesis: ( x in C & C in { (MaxADSet c) where c is Point of Y : c in A } ) thus x in C by A2; ::_thesis: C in { (MaxADSet c) where c is Point of Y : c in A } thus C in { (MaxADSet c) where c is Point of Y : c in A } by A4, A6; ::_thesis: verum end; then A7: x in MaxADSet A by TARSKI:def_4; MaxADSet A c= (MaxADSet A) \/ (MaxADSet B) by XBOOLE_1:7; hence x in (MaxADSet A) \/ (MaxADSet B) by A7; ::_thesis: verum end; supposeA8: a in B ; ::_thesis: x in (MaxADSet A) \/ (MaxADSet B) now__::_thesis:_ex_C_being_set_st_ (_x_in_C_&_C_in__{__(MaxADSet_c)_where_c_is_Point_of_Y_:_c_in_B__}__) take C = C; ::_thesis: ( x in C & C in { (MaxADSet c) where c is Point of Y : c in B } ) thus x in C by A2; ::_thesis: C in { (MaxADSet c) where c is Point of Y : c in B } thus C in { (MaxADSet c) where c is Point of Y : c in B } by A4, A8; ::_thesis: verum end; then A9: x in MaxADSet B by TARSKI:def_4; MaxADSet B c= (MaxADSet A) \/ (MaxADSet B) by XBOOLE_1:7; hence x in (MaxADSet A) \/ (MaxADSet B) by A9; ::_thesis: verum end; end; end; hence x in (MaxADSet A) \/ (MaxADSet B) ; ::_thesis: verum end; A10: MaxADSet B c= MaxADSet (A \/ B) by Th31, XBOOLE_1:7; MaxADSet A c= MaxADSet (A \/ B) by Th31, XBOOLE_1:7; then (MaxADSet A) \/ (MaxADSet B) c= MaxADSet (A \/ B) by A10, XBOOLE_1:8; hence MaxADSet (A \/ B) = (MaxADSet A) \/ (MaxADSet B) by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th37: :: TEX_4:37 for Y being non empty TopStruct for A, B being Subset of Y holds MaxADSet (A /\ B) c= (MaxADSet A) /\ (MaxADSet B) proof let Y be non empty TopStruct ; ::_thesis: for A, B being Subset of Y holds MaxADSet (A /\ B) c= (MaxADSet A) /\ (MaxADSet B) let A, B be Subset of Y; ::_thesis: MaxADSet (A /\ B) c= (MaxADSet A) /\ (MaxADSet B) A1: MaxADSet (A /\ B) c= MaxADSet B by Th31, XBOOLE_1:17; MaxADSet (A /\ B) c= MaxADSet A by Th31, XBOOLE_1:17; hence MaxADSet (A /\ B) c= (MaxADSet A) /\ (MaxADSet B) by A1, XBOOLE_1:19; ::_thesis: verum end; registration let Y be non empty TopStruct ; let A be non empty Subset of Y; cluster MaxADSet A -> non empty ; coherence not MaxADSet A is empty by Th32, XBOOLE_1:3; end; registration let Y be non empty TopStruct ; let A be empty Subset of Y; cluster MaxADSet A -> empty ; coherence MaxADSet A is empty proof now__::_thesis:_MaxADSet_A_is_empty assume not MaxADSet A is empty ; ::_thesis: contradiction then consider x being set such that A1: x in MaxADSet A by XBOOLE_0:def_1; reconsider a = x as Point of Y by A1; consider D being set such that a in D and A2: D in { (MaxADSet b) where b is Point of Y : b in A } by A1, TARSKI:def_4; ex b being Point of Y st ( D = MaxADSet b & b in A ) by A2; hence contradiction ; ::_thesis: verum end; hence MaxADSet A is empty ; ::_thesis: verum end; end; registration let Y be non empty TopStruct ; let A be non proper Subset of Y; cluster MaxADSet A -> non proper ; coherence not MaxADSet A is proper proof A = the carrier of Y by SUBSET_1:def_6; then the carrier of Y c= MaxADSet A by Th32; then MaxADSet A = the carrier of Y by XBOOLE_0:def_10; hence not MaxADSet A is proper by SUBSET_1:def_6; ::_thesis: verum end; end; registration let Y be non trivial TopStruct ; let A be non trivial Subset of Y; cluster MaxADSet A -> non trivial ; coherence not MaxADSet A is trivial proof A c= MaxADSet A by Th32; hence not MaxADSet A is trivial ; ::_thesis: verum end; end; theorem Th38: :: TEX_4:38 for Y being non empty TopStruct for G, A being Subset of Y st G is open & A c= G holds MaxADSet A c= G proof let Y be non empty TopStruct ; ::_thesis: for G, A being Subset of Y st G is open & A c= G holds MaxADSet A c= G let G, A be Subset of Y; ::_thesis: ( G is open & A c= G implies MaxADSet A c= G ) assume A1: G is open ; ::_thesis: ( not A c= G or MaxADSet A c= G ) assume A2: A c= G ; ::_thesis: MaxADSet A c= G MaxADSet A c= G proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in MaxADSet A or x in G ) assume A3: x in MaxADSet A ; ::_thesis: x in G then reconsider a = x as Point of Y ; consider D being set such that A4: a in D and A5: D in { (MaxADSet b) where b is Point of Y : b in A } by A3, TARSKI:def_4; consider b being Point of Y such that A6: D = MaxADSet b and A7: b in A by A5; A8: MaxADSet a = MaxADSet b by A4, A6, Th21; A9: {a} c= MaxADSet a by Th12; MaxADSet b c= G by A1, A2, A7, Th24; then {a} c= G by A8, A9, XBOOLE_1:1; hence x in G by ZFMISC_1:31; ::_thesis: verum end; hence MaxADSet A c= G ; ::_thesis: verum end; theorem Th39: :: TEX_4:39 for Y being non empty TopStruct for A being Subset of Y st { G where G is Subset of Y : ( G is open & A c= G ) } <> {} holds MaxADSet A c= meet { G where G is Subset of Y : ( G is open & A c= G ) } proof let Y be non empty TopStruct ; ::_thesis: for A being Subset of Y st { G where G is Subset of Y : ( G is open & A c= G ) } <> {} holds MaxADSet A c= meet { G where G is Subset of Y : ( G is open & A c= G ) } let A be Subset of Y; ::_thesis: ( { G where G is Subset of Y : ( G is open & A c= G ) } <> {} implies MaxADSet A c= meet { G where G is Subset of Y : ( G is open & A c= G ) } ) set F = { G where G is Subset of Y : ( G is open & A c= G ) } ; { G where G is Subset of Y : ( G is open & A c= G ) } c= bool the carrier of Y proof let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { G where G is Subset of Y : ( G is open & A c= G ) } or C in bool the carrier of Y ) assume C in { G where G is Subset of Y : ( G is open & A c= G ) } ; ::_thesis: C in bool the carrier of Y then ex P being Subset of Y st ( C = P & P is open & A c= P ) ; hence C in bool the carrier of Y ; ::_thesis: verum end; then reconsider F = { G where G is Subset of Y : ( G is open & A c= G ) } as Subset-Family of Y ; A1: now__::_thesis:_for_C_being_set_st_C_in_F_holds_ MaxADSet_A_c=_C let C be set ; ::_thesis: ( C in F implies MaxADSet A c= C ) assume C in F ; ::_thesis: MaxADSet A c= C then ex G being Subset of Y st ( G = C & G is open & A c= G ) ; hence MaxADSet A c= C by Th38; ::_thesis: verum end; assume { G where G is Subset of Y : ( G is open & A c= G ) } <> {} ; ::_thesis: MaxADSet A c= meet { G where G is Subset of Y : ( G is open & A c= G ) } hence MaxADSet A c= meet { G where G is Subset of Y : ( G is open & A c= G ) } by A1, SETFAM_1:5; ::_thesis: verum end; theorem Th40: :: TEX_4:40 for Y being non empty TopStruct for F, A being Subset of Y st F is closed & A c= F holds MaxADSet A c= F proof let Y be non empty TopStruct ; ::_thesis: for F, A being Subset of Y st F is closed & A c= F holds MaxADSet A c= F let F, A be Subset of Y; ::_thesis: ( F is closed & A c= F implies MaxADSet A c= F ) assume A1: F is closed ; ::_thesis: ( not A c= F or MaxADSet A c= F ) assume A2: A c= F ; ::_thesis: MaxADSet A c= F MaxADSet A c= F proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in MaxADSet A or x in F ) assume A3: x in MaxADSet A ; ::_thesis: x in F then reconsider a = x as Point of Y ; consider D being set such that A4: a in D and A5: D in { (MaxADSet b) where b is Point of Y : b in A } by A3, TARSKI:def_4; consider b being Point of Y such that A6: D = MaxADSet b and A7: b in A by A5; A8: MaxADSet a = MaxADSet b by A4, A6, Th21; A9: {a} c= MaxADSet a by Th12; MaxADSet b c= F by A1, A2, A7, Th23; then {a} c= F by A8, A9, XBOOLE_1:1; hence x in F by ZFMISC_1:31; ::_thesis: verum end; hence MaxADSet A c= F ; ::_thesis: verum end; theorem Th41: :: TEX_4:41 for Y being non empty TopStruct for A being Subset of Y st { F where F is Subset of Y : ( F is closed & A c= F ) } <> {} holds MaxADSet A c= meet { F where F is Subset of Y : ( F is closed & A c= F ) } proof let Y be non empty TopStruct ; ::_thesis: for A being Subset of Y st { F where F is Subset of Y : ( F is closed & A c= F ) } <> {} holds MaxADSet A c= meet { F where F is Subset of Y : ( F is closed & A c= F ) } let A be Subset of Y; ::_thesis: ( { F where F is Subset of Y : ( F is closed & A c= F ) } <> {} implies MaxADSet A c= meet { F where F is Subset of Y : ( F is closed & A c= F ) } ) set G = { F where F is Subset of Y : ( F is closed & A c= F ) } ; { F where F is Subset of Y : ( F is closed & A c= F ) } c= bool the carrier of Y proof let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { F where F is Subset of Y : ( F is closed & A c= F ) } or C in bool the carrier of Y ) assume C in { F where F is Subset of Y : ( F is closed & A c= F ) } ; ::_thesis: C in bool the carrier of Y then ex P being Subset of Y st ( C = P & P is closed & A c= P ) ; hence C in bool the carrier of Y ; ::_thesis: verum end; then reconsider G = { F where F is Subset of Y : ( F is closed & A c= F ) } as Subset-Family of Y ; A1: now__::_thesis:_for_C_being_set_st_C_in_G_holds_ MaxADSet_A_c=_C let C be set ; ::_thesis: ( C in G implies MaxADSet A c= C ) assume C in G ; ::_thesis: MaxADSet A c= C then ex F being Subset of Y st ( F = C & F is closed & A c= F ) ; hence MaxADSet A c= C by Th40; ::_thesis: verum end; assume { F where F is Subset of Y : ( F is closed & A c= F ) } <> {} ; ::_thesis: MaxADSet A c= meet { F where F is Subset of Y : ( F is closed & A c= F ) } hence MaxADSet A c= meet { F where F is Subset of Y : ( F is closed & A c= F ) } by A1, SETFAM_1:5; ::_thesis: verum end; begin definition let X be non empty TopSpace; let A be Subset of X; redefine attr A is anti-discrete means :Def12: :: TEX_4:def 12 for x being Point of X st x in A holds A c= Cl {x}; compatibility ( A is anti-discrete iff for x being Point of X st x in A holds A c= Cl {x} ) proof thus ( A is anti-discrete implies for x being Point of X st x in A holds A c= Cl {x} ) ::_thesis: ( ( for x being Point of X st x in A holds A c= Cl {x} ) implies A is anti-discrete ) proof assume A1: A is anti-discrete ; ::_thesis: for x being Point of X st x in A holds A c= Cl {x} let x be Point of X; ::_thesis: ( x in A implies A c= Cl {x} ) assume A2: x in A ; ::_thesis: A c= Cl {x} {x} c= Cl {x} by PRE_TOPC:18; then A3: x in Cl {x} by ZFMISC_1:31; ( A misses Cl {x} or A c= Cl {x} ) by A1, Def4; hence A c= Cl {x} by A2, A3, XBOOLE_0:3; ::_thesis: verum end; thus ( ( for x being Point of X st x in A holds A c= Cl {x} ) implies A is anti-discrete ) ::_thesis: verum proof assume A4: for x being Point of X st x in A holds A c= Cl {x} ; ::_thesis: A is anti-discrete now__::_thesis:_for_F_being_Subset_of_X_st_F_is_closed_&_A_meets_F_holds_ A_c=_F let F be Subset of X; ::_thesis: ( F is closed & A meets F implies A c= F ) assume A5: F is closed ; ::_thesis: ( A meets F implies A c= F ) assume A meets F ; ::_thesis: A c= F then consider a being set such that A6: a in A /\ F by XBOOLE_0:4; reconsider a = a as Point of X by A6; a in F by A6, XBOOLE_0:def_4; then {a} c= F by ZFMISC_1:31; then A7: Cl {a} c= F by A5, TOPS_1:5; a in A by A6, XBOOLE_0:def_4; then A c= Cl {a} by A4; hence A c= F by A7, XBOOLE_1:1; ::_thesis: verum end; hence A is anti-discrete by Def4; ::_thesis: verum end; end; end; :: deftheorem Def12 defines anti-discrete TEX_4:def_12_:_ for X being non empty TopSpace for A being Subset of X holds ( A is anti-discrete iff for x being Point of X st x in A holds A c= Cl {x} ); definition let X be non empty TopSpace; let A be Subset of X; redefine attr A is anti-discrete means :: TEX_4:def 13 for x being Point of X st x in A holds Cl A = Cl {x}; compatibility ( A is anti-discrete iff for x being Point of X st x in A holds Cl A = Cl {x} ) proof thus ( A is anti-discrete implies for x being Point of X st x in A holds Cl A = Cl {x} ) ::_thesis: ( ( for x being Point of X st x in A holds Cl A = Cl {x} ) implies A is anti-discrete ) proof assume A1: A is anti-discrete ; ::_thesis: for x being Point of X st x in A holds Cl A = Cl {x} let x be Point of X; ::_thesis: ( x in A implies Cl A = Cl {x} ) assume A2: x in A ; ::_thesis: Cl A = Cl {x} then {x} c= A by ZFMISC_1:31; then A3: Cl {x} c= Cl A by PRE_TOPC:19; A c= Cl {x} by A1, A2, Def12; then Cl A c= Cl {x} by TOPS_1:5; hence Cl A = Cl {x} by A3, XBOOLE_0:def_10; ::_thesis: verum end; assume A4: for x being Point of X st x in A holds Cl A = Cl {x} ; ::_thesis: A is anti-discrete now__::_thesis:_for_x_being_Point_of_X_st_x_in_A_holds_ A_c=_Cl_{x} let x be Point of X; ::_thesis: ( x in A implies A c= Cl {x} ) assume x in A ; ::_thesis: A c= Cl {x} then Cl A = Cl {x} by A4; hence A c= Cl {x} by PRE_TOPC:18; ::_thesis: verum end; hence A is anti-discrete by Def12; ::_thesis: verum end; end; :: deftheorem defines anti-discrete TEX_4:def_13_:_ for X being non empty TopSpace for A being Subset of X holds ( A is anti-discrete iff for x being Point of X st x in A holds Cl A = Cl {x} ); definition let X be non empty TopSpace; let A be Subset of X; redefine attr A is anti-discrete means :Def14: :: TEX_4:def 14 for x, y being Point of X st x in A & y in A holds Cl {x} = Cl {y}; compatibility ( A is anti-discrete iff for x, y being Point of X st x in A & y in A holds Cl {x} = Cl {y} ) proof thus ( A is anti-discrete implies for x, y being Point of X st x in A & y in A holds Cl {x} = Cl {y} ) ::_thesis: ( ( for x, y being Point of X st x in A & y in A holds Cl {x} = Cl {y} ) implies A is anti-discrete ) proof assume A1: A is anti-discrete ; ::_thesis: for x, y being Point of X st x in A & y in A holds Cl {x} = Cl {y} let x, y be Point of X; ::_thesis: ( x in A & y in A implies Cl {x} = Cl {y} ) assume that A2: x in A and A3: y in A ; ::_thesis: Cl {x} = Cl {y} A c= Cl {y} by A1, A3, Def12; then {x} c= Cl {y} by A2, ZFMISC_1:31; then A4: Cl {x} c= Cl {y} by TOPS_1:5; A c= Cl {x} by A1, A2, Def12; then {y} c= Cl {x} by A3, ZFMISC_1:31; then Cl {y} c= Cl {x} by TOPS_1:5; hence Cl {x} = Cl {y} by A4, XBOOLE_0:def_10; ::_thesis: verum end; thus ( ( for x, y being Point of X st x in A & y in A holds Cl {x} = Cl {y} ) implies A is anti-discrete ) ::_thesis: verum proof assume A5: for x, y being Point of X st x in A & y in A holds Cl {x} = Cl {y} ; ::_thesis: A is anti-discrete now__::_thesis:_for_x_being_Point_of_X_st_x_in_A_holds_ A_c=_Cl_{x} let x be Point of X; ::_thesis: ( x in A implies A c= Cl {x} ) assume A6: x in A ; ::_thesis: A c= Cl {x} now__::_thesis:_for_a_being_set_st_a_in_A_holds_ a_in_Cl_{x} let a be set ; ::_thesis: ( a in A implies a in Cl {x} ) assume A7: a in A ; ::_thesis: a in Cl {x} then reconsider y = a as Point of X ; {y} c= Cl {y} by PRE_TOPC:18; then y in Cl {y} by ZFMISC_1:31; hence a in Cl {x} by A5, A6, A7; ::_thesis: verum end; hence A c= Cl {x} by TARSKI:def_3; ::_thesis: verum end; hence A is anti-discrete by Def12; ::_thesis: verum end; end; end; :: deftheorem Def14 defines anti-discrete TEX_4:def_14_:_ for X being non empty TopSpace for A being Subset of X holds ( A is anti-discrete iff for x, y being Point of X st x in A & y in A holds Cl {x} = Cl {y} ); theorem :: TEX_4:42 for X being non empty TopSpace for x being Point of X for D being Subset of X st D is anti-discrete & Cl {x} c= D holds D = Cl {x} proof let X be non empty TopSpace; ::_thesis: for x being Point of X for D being Subset of X st D is anti-discrete & Cl {x} c= D holds D = Cl {x} let x be Point of X; ::_thesis: for D being Subset of X st D is anti-discrete & Cl {x} c= D holds D = Cl {x} let D be Subset of X; ::_thesis: ( D is anti-discrete & Cl {x} c= D implies D = Cl {x} ) assume D is anti-discrete ; ::_thesis: ( not Cl {x} c= D or D = Cl {x} ) then ( D misses Cl {x} or D c= Cl {x} ) by Def4; then A1: ( D /\ (Cl {x}) = {} or D c= Cl {x} ) by XBOOLE_0:def_7; assume Cl {x} c= D ; ::_thesis: D = Cl {x} hence D = Cl {x} by A1, XBOOLE_0:def_10, XBOOLE_1:28; ::_thesis: verum end; theorem :: TEX_4:43 for X being non empty TopSpace for A being Subset of X holds ( ( A is anti-discrete & A is closed ) iff for x being Point of X st x in A holds A = Cl {x} ) proof let X be non empty TopSpace; ::_thesis: for A being Subset of X holds ( ( A is anti-discrete & A is closed ) iff for x being Point of X st x in A holds A = Cl {x} ) let A be Subset of X; ::_thesis: ( ( A is anti-discrete & A is closed ) iff for x being Point of X st x in A holds A = Cl {x} ) thus ( A is anti-discrete & A is closed implies for x being Point of X st x in A holds A = Cl {x} ) ::_thesis: ( ( for x being Point of X st x in A holds A = Cl {x} ) implies ( A is anti-discrete & A is closed ) ) proof assume A1: A is anti-discrete ; ::_thesis: ( not A is closed or for x being Point of X st x in A holds A = Cl {x} ) assume A2: A is closed ; ::_thesis: for x being Point of X st x in A holds A = Cl {x} let x be Point of X; ::_thesis: ( x in A implies A = Cl {x} ) assume A3: x in A ; ::_thesis: A = Cl {x} then {x} c= A by ZFMISC_1:31; then A4: Cl {x} c= A by A2, TOPS_1:5; A c= Cl {x} by A1, A3, Def12; hence A = Cl {x} by A4, XBOOLE_0:def_10; ::_thesis: verum end; thus ( ( for x being Point of X st x in A holds A = Cl {x} ) implies ( A is anti-discrete & A is closed ) ) ::_thesis: verum proof assume A5: for x being Point of X st x in A holds A = Cl {x} ; ::_thesis: ( A is anti-discrete & A is closed ) then for x being Point of X st x in A holds A c= Cl {x} ; hence A is anti-discrete by Def12; ::_thesis: A is closed hereby ::_thesis: verum percases ( A is empty or not A is empty ) ; suppose A is empty ; ::_thesis: A is closed hence A is closed ; ::_thesis: verum end; suppose not A is empty ; ::_thesis: A is closed then consider a being set such that A6: a in A by XBOOLE_0:def_1; reconsider a = a as Point of X by A6; A = Cl {a} by A5, A6; hence A is closed ; ::_thesis: verum end; end; end; end; end; theorem :: TEX_4:44 for X being non empty TopSpace for A being Subset of X st A is anti-discrete & not A is open holds A is boundary proof let X be non empty TopSpace; ::_thesis: for A being Subset of X st A is anti-discrete & not A is open holds A is boundary let A be Subset of X; ::_thesis: ( A is anti-discrete & not A is open implies A is boundary ) A1: Int A c= A by TOPS_1:16; assume A is anti-discrete ; ::_thesis: ( A is open or A is boundary ) then ( A misses Int A or A c= Int A ) by Def3; then A2: ( A /\ (Int A) = {} or A c= Int A ) by XBOOLE_0:def_7; assume A3: not A is open ; ::_thesis: A is boundary assume not A is boundary ; ::_thesis: contradiction then Int A <> {} by TOPS_1:48; hence contradiction by A3, A2, A1, XBOOLE_0:def_10, XBOOLE_1:28; ::_thesis: verum end; theorem Th45: :: TEX_4:45 for X being non empty TopSpace for x being Point of X st Cl {x} = {x} holds {x} is maximal_anti-discrete proof let X be non empty TopSpace; ::_thesis: for x being Point of X st Cl {x} = {x} holds {x} is maximal_anti-discrete let x be Point of X; ::_thesis: ( Cl {x} = {x} implies {x} is maximal_anti-discrete ) assume A1: Cl {x} = {x} ; ::_thesis: {x} is maximal_anti-discrete {x} is anti-discrete by Th6; hence {x} is maximal_anti-discrete by A1, Th17; ::_thesis: verum end; theorem Th46: :: TEX_4:46 for X being non empty TopSpace for x being Point of X holds MaxADSet x c= meet { G where G is Subset of X : ( G is open & x in G ) } proof let X be non empty TopSpace; ::_thesis: for x being Point of X holds MaxADSet x c= meet { G where G is Subset of X : ( G is open & x in G ) } let x be Point of X; ::_thesis: MaxADSet x c= meet { G where G is Subset of X : ( G is open & x in G ) } set F = { G where G is Subset of X : ( G is open & x in G ) } ; { G where G is Subset of X : ( G is open & x in G ) } c= bool the carrier of X proof let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { G where G is Subset of X : ( G is open & x in G ) } or C in bool the carrier of X ) assume C in { G where G is Subset of X : ( G is open & x in G ) } ; ::_thesis: C in bool the carrier of X then ex P being Subset of X st ( C = P & P is open & x in P ) ; hence C in bool the carrier of X ; ::_thesis: verum end; then reconsider F = { G where G is Subset of X : ( G is open & x in G ) } as Subset-Family of X ; now__::_thesis:_for_C_being_set_st_C_in_F_holds_ MaxADSet_x_c=_C let C be set ; ::_thesis: ( C in F implies MaxADSet x c= C ) assume C in F ; ::_thesis: MaxADSet x c= C then ex G being Subset of X st ( G = C & G is open & x in G ) ; hence MaxADSet x c= C by Th24; ::_thesis: verum end; hence MaxADSet x c= meet { G where G is Subset of X : ( G is open & x in G ) } by SETFAM_1:5; ::_thesis: verum end; theorem Th47: :: TEX_4:47 for X being non empty TopSpace for x being Point of X holds MaxADSet x c= meet { F where F is Subset of X : ( F is closed & x in F ) } proof let X be non empty TopSpace; ::_thesis: for x being Point of X holds MaxADSet x c= meet { F where F is Subset of X : ( F is closed & x in F ) } let x be Point of X; ::_thesis: MaxADSet x c= meet { F where F is Subset of X : ( F is closed & x in F ) } set G = { F where F is Subset of X : ( F is closed & x in F ) } ; { F where F is Subset of X : ( F is closed & x in F ) } c= bool the carrier of X proof let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { F where F is Subset of X : ( F is closed & x in F ) } or C in bool the carrier of X ) assume C in { F where F is Subset of X : ( F is closed & x in F ) } ; ::_thesis: C in bool the carrier of X then ex P being Subset of X st ( C = P & P is closed & x in P ) ; hence C in bool the carrier of X ; ::_thesis: verum end; then reconsider G = { F where F is Subset of X : ( F is closed & x in F ) } as Subset-Family of X ; now__::_thesis:_for_C_being_set_st_C_in_G_holds_ MaxADSet_x_c=_C let C be set ; ::_thesis: ( C in G implies MaxADSet x c= C ) assume C in G ; ::_thesis: MaxADSet x c= C then ex F being Subset of X st ( F = C & F is closed & x in F ) ; hence MaxADSet x c= C by Th23; ::_thesis: verum end; hence MaxADSet x c= meet { F where F is Subset of X : ( F is closed & x in F ) } by SETFAM_1:5; ::_thesis: verum end; theorem Th48: :: TEX_4:48 for X being non empty TopSpace for x being Point of X holds MaxADSet x c= Cl {x} proof let X be non empty TopSpace; ::_thesis: for x being Point of X holds MaxADSet x c= Cl {x} let x be Point of X; ::_thesis: MaxADSet x c= Cl {x} Cl {x} = meet { F where F is Subset of X : ( F is closed & x in F ) } by Th2; hence MaxADSet x c= Cl {x} by Th47; ::_thesis: verum end; Lm1: for X being non empty TopSpace for x, y being Point of X st MaxADSet x = MaxADSet y holds Cl {x} = Cl {y} proof let X be non empty TopSpace; ::_thesis: for x, y being Point of X st MaxADSet x = MaxADSet y holds Cl {x} = Cl {y} let x, y be Point of X; ::_thesis: ( MaxADSet x = MaxADSet y implies Cl {x} = Cl {y} ) assume A1: MaxADSet x = MaxADSet y ; ::_thesis: Cl {x} = Cl {y} then A2: y in MaxADSet x by Th21; MaxADSet y is maximal_anti-discrete by Th20; then A3: MaxADSet y is anti-discrete by Def7; x in MaxADSet y by A1, Th21; hence Cl {x} = Cl {y} by A1, A2, A3, Def14; ::_thesis: verum end; theorem Th49: :: TEX_4:49 for X being non empty TopSpace for x, y being Point of X holds ( MaxADSet x = MaxADSet y iff Cl {x} = Cl {y} ) proof let X be non empty TopSpace; ::_thesis: for x, y being Point of X holds ( MaxADSet x = MaxADSet y iff Cl {x} = Cl {y} ) let x, y be Point of X; ::_thesis: ( MaxADSet x = MaxADSet y iff Cl {x} = Cl {y} ) A1: MaxADSet x c= (MaxADSet x) \/ (MaxADSet y) by XBOOLE_1:7; thus ( MaxADSet x = MaxADSet y implies Cl {x} = Cl {y} ) by Lm1; ::_thesis: ( Cl {x} = Cl {y} implies MaxADSet x = MaxADSet y ) A2: MaxADSet y c= (MaxADSet x) \/ (MaxADSet y) by XBOOLE_1:7; assume A3: Cl {x} = Cl {y} ; ::_thesis: MaxADSet x = MaxADSet y now__::_thesis:_for_a_being_Point_of_X_st_a_in_(MaxADSet_x)_\/_(MaxADSet_y)_holds_ (MaxADSet_x)_\/_(MaxADSet_y)_c=_Cl_{a} let a be Point of X; ::_thesis: ( a in (MaxADSet x) \/ (MaxADSet y) implies (MaxADSet x) \/ (MaxADSet y) c= Cl {a} ) assume A4: a in (MaxADSet x) \/ (MaxADSet y) ; ::_thesis: (MaxADSet x) \/ (MaxADSet y) c= Cl {a} now__::_thesis:_(MaxADSet_x)_\/_(MaxADSet_y)_c=_Cl_{a} percases ( a in MaxADSet x or a in MaxADSet y ) by A4, XBOOLE_0:def_3; suppose a in MaxADSet x ; ::_thesis: (MaxADSet x) \/ (MaxADSet y) c= Cl {a} then A5: MaxADSet a = MaxADSet x by Th21; then Cl {a} = Cl {x} by Lm1; then A6: MaxADSet y c= Cl {a} by A3, Th48; MaxADSet x c= Cl {a} by A5, Th48; hence (MaxADSet x) \/ (MaxADSet y) c= Cl {a} by A6, XBOOLE_1:8; ::_thesis: verum end; suppose a in MaxADSet y ; ::_thesis: (MaxADSet x) \/ (MaxADSet y) c= Cl {a} then A7: MaxADSet a = MaxADSet y by Th21; then Cl {a} = Cl {y} by Lm1; then A8: MaxADSet x c= Cl {a} by A3, Th48; MaxADSet y c= Cl {a} by A7, Th48; hence (MaxADSet x) \/ (MaxADSet y) c= Cl {a} by A8, XBOOLE_1:8; ::_thesis: verum end; end; end; hence (MaxADSet x) \/ (MaxADSet y) c= Cl {a} ; ::_thesis: verum end; then A9: (MaxADSet x) \/ (MaxADSet y) is anti-discrete by Def12; A10: MaxADSet y is maximal_anti-discrete by Th20; MaxADSet x is maximal_anti-discrete by Th20; then MaxADSet x = (MaxADSet x) \/ (MaxADSet y) by A9, A1, Def7; hence MaxADSet x = MaxADSet y by A9, A10, A2, Def7; ::_thesis: verum end; theorem :: TEX_4:50 for X being non empty TopSpace for x, y being Point of X holds ( MaxADSet x misses MaxADSet y iff Cl {x} <> Cl {y} ) proof let X be non empty TopSpace; ::_thesis: for x, y being Point of X holds ( MaxADSet x misses MaxADSet y iff Cl {x} <> Cl {y} ) let x, y be Point of X; ::_thesis: ( MaxADSet x misses MaxADSet y iff Cl {x} <> Cl {y} ) thus ( MaxADSet x misses MaxADSet y implies Cl {x} <> Cl {y} ) by Th49; ::_thesis: ( Cl {x} <> Cl {y} implies MaxADSet x misses MaxADSet y ) assume A1: Cl {x} <> Cl {y} ; ::_thesis: MaxADSet x misses MaxADSet y assume MaxADSet x meets MaxADSet y ; ::_thesis: contradiction then MaxADSet x = MaxADSet y by Th22; hence contradiction by A1, Th49; ::_thesis: verum end; definition let X be non empty TopSpace; let x be Point of X; :: original: MaxADSet redefine func MaxADSet x -> non empty Subset of X equals :: TEX_4:def 15 (Cl {x}) /\ (meet { G where G is Subset of X : ( G is open & x in G ) } ); compatibility for b1 being non empty Subset of X holds ( b1 = MaxADSet x iff b1 = (Cl {x}) /\ (meet { G where G is Subset of X : ( G is open & x in G ) } ) ) proof set F = { G where G is Subset of X : ( G is open & x in G ) } ; { G where G is Subset of X : ( G is open & x in G ) } c= bool the carrier of X proof let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { G where G is Subset of X : ( G is open & x in G ) } or C in bool the carrier of X ) assume C in { G where G is Subset of X : ( G is open & x in G ) } ; ::_thesis: C in bool the carrier of X then ex P being Subset of X st ( C = P & P is open & x in P ) ; hence C in bool the carrier of X ; ::_thesis: verum end; then reconsider F = { G where G is Subset of X : ( G is open & x in G ) } as Subset-Family of X ; A1: MaxADSet x c= Cl {x} by Th48; A2: (Cl {x}) /\ (meet F) c= MaxADSet x proof assume not (Cl {x}) /\ (meet F) c= MaxADSet x ; ::_thesis: contradiction then ((Cl {x}) /\ (meet F)) \ (MaxADSet x) <> {} by XBOOLE_1:37; then consider a being set such that A3: a in ((Cl {x}) /\ (meet F)) \ (MaxADSet x) by XBOOLE_0:def_1; A4: a in (Cl {x}) /\ (meet F) by A3, XBOOLE_0:def_5; reconsider a = a as Point of X by A3; not a in MaxADSet x by A3, XBOOLE_0:def_5; then A5: MaxADSet a <> MaxADSet x by Th21; now__::_thesis:_x_in_Cl_{a} set G = (Cl {a}) ` ; {a} c= Cl {a} by PRE_TOPC:18; then A6: a in Cl {a} by ZFMISC_1:31; assume not x in Cl {a} ; ::_thesis: contradiction then x in (Cl {a}) ` by SUBSET_1:29; then (Cl {a}) ` in F ; then A7: meet F c= (Cl {a}) ` by SETFAM_1:3; a in meet F by A4, XBOOLE_0:def_4; hence contradiction by A7, A6, XBOOLE_0:def_5; ::_thesis: verum end; then {x} c= Cl {a} by ZFMISC_1:31; then A8: Cl {x} c= Cl {a} by TOPS_1:5; a in Cl {x} by A4, XBOOLE_0:def_4; then {a} c= Cl {x} by ZFMISC_1:31; then Cl {a} c= Cl {x} by TOPS_1:5; then Cl {x} = Cl {a} by A8, XBOOLE_0:def_10; hence contradiction by A5, Th49; ::_thesis: verum end; MaxADSet x c= meet F by Th46; then MaxADSet x c= (Cl {x}) /\ (meet F) by A1, XBOOLE_1:19; hence for b1 being non empty Subset of X holds ( b1 = MaxADSet x iff b1 = (Cl {x}) /\ (meet { G where G is Subset of X : ( G is open & x in G ) } ) ) by A2, XBOOLE_0:def_10; ::_thesis: verum end; coherence MaxADSet x is non empty Subset of X ; end; :: deftheorem defines MaxADSet TEX_4:def_15_:_ for X being non empty TopSpace for x being Point of X holds MaxADSet x = (Cl {x}) /\ (meet { G where G is Subset of X : ( G is open & x in G ) } ); theorem Th51: :: TEX_4:51 for X being non empty TopSpace for x, y being Point of X holds ( Cl {x} c= Cl {y} iff meet { G where G is Subset of X : ( G is open & y in G ) } c= meet { G where G is Subset of X : ( G is open & x in G ) } ) proof let X be non empty TopSpace; ::_thesis: for x, y being Point of X holds ( Cl {x} c= Cl {y} iff meet { G where G is Subset of X : ( G is open & y in G ) } c= meet { G where G is Subset of X : ( G is open & x in G ) } ) let x, y be Point of X; ::_thesis: ( Cl {x} c= Cl {y} iff meet { G where G is Subset of X : ( G is open & y in G ) } c= meet { G where G is Subset of X : ( G is open & x in G ) } ) set FX = { G where G is Subset of X : ( G is open & x in G ) } ; set FY = { G where G is Subset of X : ( G is open & y in G ) } ; A1: [#] X in { G where G is Subset of X : ( G is open & x in G ) } ; thus ( Cl {x} c= Cl {y} implies meet { G where G is Subset of X : ( G is open & y in G ) } c= meet { G where G is Subset of X : ( G is open & x in G ) } ) ::_thesis: ( meet { G where G is Subset of X : ( G is open & y in G ) } c= meet { G where G is Subset of X : ( G is open & x in G ) } implies Cl {x} c= Cl {y} ) proof assume A2: Cl {x} c= Cl {y} ; ::_thesis: meet { G where G is Subset of X : ( G is open & y in G ) } c= meet { G where G is Subset of X : ( G is open & x in G ) } now__::_thesis:_for_P_being_set_st_P_in__{__G_where_G_is_Subset_of_X_:_(_G_is_open_&_x_in_G_)__}__holds_ P_in__{__G_where_G_is_Subset_of_X_:_(_G_is_open_&_y_in_G_)__}_ let P be set ; ::_thesis: ( P in { G where G is Subset of X : ( G is open & x in G ) } implies P in { G where G is Subset of X : ( G is open & y in G ) } ) assume P in { G where G is Subset of X : ( G is open & x in G ) } ; ::_thesis: P in { G where G is Subset of X : ( G is open & y in G ) } then consider G being Subset of X such that A3: G = P and A4: G is open and A5: x in G ; now__::_thesis:_y_in_G assume not y in G ; ::_thesis: contradiction then {y} misses G by ZFMISC_1:50; then A6: Cl {y} misses G by A4, TSEP_1:36; {x} c= Cl {x} by PRE_TOPC:18; then x in Cl {x} by ZFMISC_1:31; hence contradiction by A2, A5, A6, XBOOLE_0:3; ::_thesis: verum end; hence P in { G where G is Subset of X : ( G is open & y in G ) } by A3, A4; ::_thesis: verum end; then { G where G is Subset of X : ( G is open & x in G ) } c= { G where G is Subset of X : ( G is open & y in G ) } by TARSKI:def_3; hence meet { G where G is Subset of X : ( G is open & y in G ) } c= meet { G where G is Subset of X : ( G is open & x in G ) } by A1, SETFAM_1:6; ::_thesis: verum end; assume A7: meet { G where G is Subset of X : ( G is open & y in G ) } c= meet { G where G is Subset of X : ( G is open & x in G ) } ; ::_thesis: Cl {x} c= Cl {y} set G = (Cl {y}) ` ; assume A8: not Cl {x} c= Cl {y} ; ::_thesis: contradiction now__::_thesis:_not_x_in_Cl_{y} assume x in Cl {y} ; ::_thesis: contradiction then {x} c= Cl {y} by ZFMISC_1:31; hence contradiction by A8, TOPS_1:5; ::_thesis: verum end; then x in (Cl {y}) ` by SUBSET_1:29; then (Cl {y}) ` in { G where G is Subset of X : ( G is open & x in G ) } ; then meet { G where G is Subset of X : ( G is open & x in G ) } c= (Cl {y}) ` by SETFAM_1:3; then A9: meet { G where G is Subset of X : ( G is open & y in G ) } c= (Cl {y}) ` by A7, XBOOLE_1:1; {y} c= Cl {y} by PRE_TOPC:18; then A10: y in Cl {y} by ZFMISC_1:31; {y} c= MaxADSet y by Th12; then A11: y in MaxADSet y by ZFMISC_1:31; MaxADSet y c= meet { G where G is Subset of X : ( G is open & y in G ) } by Th46; then y in meet { G where G is Subset of X : ( G is open & y in G ) } by A11; hence contradiction by A9, A10, XBOOLE_0:def_5; ::_thesis: verum end; theorem :: TEX_4:52 for X being non empty TopSpace for x, y being Point of X holds ( Cl {x} c= Cl {y} iff MaxADSet y c= meet { G where G is Subset of X : ( G is open & x in G ) } ) proof let X be non empty TopSpace; ::_thesis: for x, y being Point of X holds ( Cl {x} c= Cl {y} iff MaxADSet y c= meet { G where G is Subset of X : ( G is open & x in G ) } ) let x, y be Point of X; ::_thesis: ( Cl {x} c= Cl {y} iff MaxADSet y c= meet { G where G is Subset of X : ( G is open & x in G ) } ) set FY = { G where G is Subset of X : ( G is open & y in G ) } ; { G where G is Subset of X : ( G is open & y in G ) } c= bool the carrier of X proof let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { G where G is Subset of X : ( G is open & y in G ) } or C in bool the carrier of X ) assume C in { G where G is Subset of X : ( G is open & y in G ) } ; ::_thesis: C in bool the carrier of X then ex P being Subset of X st ( C = P & P is open & y in P ) ; hence C in bool the carrier of X ; ::_thesis: verum end; then reconsider FY = { G where G is Subset of X : ( G is open & y in G ) } as Subset-Family of X ; set FX = { G where G is Subset of X : ( G is open & x in G ) } ; { G where G is Subset of X : ( G is open & x in G ) } c= bool the carrier of X proof let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { G where G is Subset of X : ( G is open & x in G ) } or C in bool the carrier of X ) assume C in { G where G is Subset of X : ( G is open & x in G ) } ; ::_thesis: C in bool the carrier of X then ex P being Subset of X st ( C = P & P is open & x in P ) ; hence C in bool the carrier of X ; ::_thesis: verum end; then reconsider FX = { G where G is Subset of X : ( G is open & x in G ) } as Subset-Family of X ; thus ( Cl {x} c= Cl {y} implies MaxADSet y c= meet { G where G is Subset of X : ( G is open & x in G ) } ) ::_thesis: ( MaxADSet y c= meet { G where G is Subset of X : ( G is open & x in G ) } implies Cl {x} c= Cl {y} ) proof assume Cl {x} c= Cl {y} ; ::_thesis: MaxADSet y c= meet { G where G is Subset of X : ( G is open & x in G ) } then A1: meet FY c= meet FX by Th51; (Cl {y}) /\ (meet FY) c= meet FY by XBOOLE_1:17; hence MaxADSet y c= meet { G where G is Subset of X : ( G is open & x in G ) } by A1, XBOOLE_1:1; ::_thesis: verum end; {y} c= MaxADSet y by Th12; then A2: y in MaxADSet y by ZFMISC_1:31; assume MaxADSet y c= meet { G where G is Subset of X : ( G is open & x in G ) } ; ::_thesis: Cl {x} c= Cl {y} then A3: y in meet FX by A2; set G = (Cl {y}) ` ; assume A4: not Cl {x} c= Cl {y} ; ::_thesis: contradiction now__::_thesis:_not_x_in_Cl_{y} assume x in Cl {y} ; ::_thesis: contradiction then {x} c= Cl {y} by ZFMISC_1:31; hence contradiction by A4, TOPS_1:5; ::_thesis: verum end; then x in (Cl {y}) ` by SUBSET_1:29; then (Cl {y}) ` in FX ; then A5: meet FX c= (Cl {y}) ` by SETFAM_1:3; {y} c= Cl {y} by PRE_TOPC:18; then y in Cl {y} by ZFMISC_1:31; hence contradiction by A5, A3, XBOOLE_0:def_5; ::_thesis: verum end; theorem Th53: :: TEX_4:53 for X being non empty TopSpace for x, y being Point of X holds ( MaxADSet x misses MaxADSet y iff ( ex V being Subset of X st ( V is open & MaxADSet x c= V & V misses MaxADSet y ) or ex W being Subset of X st ( W is open & W misses MaxADSet x & MaxADSet y c= W ) ) ) proof let X be non empty TopSpace; ::_thesis: for x, y being Point of X holds ( MaxADSet x misses MaxADSet y iff ( ex V being Subset of X st ( V is open & MaxADSet x c= V & V misses MaxADSet y ) or ex W being Subset of X st ( W is open & W misses MaxADSet x & MaxADSet y c= W ) ) ) let x, y be Point of X; ::_thesis: ( MaxADSet x misses MaxADSet y iff ( ex V being Subset of X st ( V is open & MaxADSet x c= V & V misses MaxADSet y ) or ex W being Subset of X st ( W is open & W misses MaxADSet x & MaxADSet y c= W ) ) ) thus ( not MaxADSet x misses MaxADSet y or ex V being Subset of X st ( V is open & MaxADSet x c= V & V misses MaxADSet y ) or ex W being Subset of X st ( W is open & W misses MaxADSet x & MaxADSet y c= W ) ) ::_thesis: ( ( ex V being Subset of X st ( V is open & MaxADSet x c= V & V misses MaxADSet y ) or ex W being Subset of X st ( W is open & W misses MaxADSet x & MaxADSet y c= W ) ) implies MaxADSet x misses MaxADSet y ) proof set V = (Cl {y}) ` ; set W = (Cl {x}) ` ; assume A1: (MaxADSet x) /\ (MaxADSet y) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: ( ex V being Subset of X st ( V is open & MaxADSet x c= V & V misses MaxADSet y ) or ex W being Subset of X st ( W is open & W misses MaxADSet x & MaxADSet y c= W ) ) assume A2: for V being Subset of X st V is open & MaxADSet x c= V holds V meets MaxADSet y ; ::_thesis: ex W being Subset of X st ( W is open & W misses MaxADSet x & MaxADSet y c= W ) now__::_thesis:_ex_W_being_Element_of_bool_the_carrier_of_X_st_ (_W_is_open_&_W_misses_MaxADSet_x_&_MaxADSet_y_c=_W_) take W = (Cl {x}) ` ; ::_thesis: ( W is open & W misses MaxADSet x & MaxADSet y c= W ) thus W is open ; ::_thesis: ( W misses MaxADSet x & MaxADSet y c= W ) MaxADSet x c= Cl {x} by Th48; hence W misses MaxADSet x by SUBSET_1:24; ::_thesis: MaxADSet y c= W now__::_thesis:_MaxADSet_y_c=_W MaxADSet y c= Cl {y} by Th48; then (Cl {y}) ` misses MaxADSet y by SUBSET_1:24; then not MaxADSet x c= (Cl {y}) ` by A2; then (MaxADSet x) \ ((Cl {y}) `) <> {} by XBOOLE_1:37; then consider b being set such that A3: b in (MaxADSet x) \ ((Cl {y}) `) by XBOOLE_0:def_1; A4: b in MaxADSet x by A3, XBOOLE_0:def_5; reconsider b = b as Point of X by A3; not b in (Cl {y}) ` by A3, XBOOLE_0:def_5; then b in Cl {y} by SUBSET_1:29; then A5: {b} c= Cl {y} by ZFMISC_1:31; MaxADSet b = MaxADSet x by A4, Th21; then Cl {b} = Cl {x} by Th49; then A6: Cl {x} c= Cl {y} by A5, TOPS_1:5; assume not MaxADSet y c= W ; ::_thesis: contradiction then (MaxADSet y) \ W <> {} by XBOOLE_1:37; then consider a being set such that A7: a in (MaxADSet y) \ W by XBOOLE_0:def_1; A8: a in MaxADSet y by A7, XBOOLE_0:def_5; reconsider a = a as Point of X by A7; not a in W by A7, XBOOLE_0:def_5; then a in Cl {x} by SUBSET_1:29; then A9: {a} c= Cl {x} by ZFMISC_1:31; MaxADSet a = MaxADSet y by A8, Th21; then Cl {a} = Cl {y} by Th49; then Cl {y} c= Cl {x} by A9, TOPS_1:5; then Cl {x} = Cl {y} by A6, XBOOLE_0:def_10; then MaxADSet x = MaxADSet y by Th49; hence contradiction by A1; ::_thesis: verum end; hence MaxADSet y c= W ; ::_thesis: verum end; hence ex W being Subset of X st ( W is open & W misses MaxADSet x & MaxADSet y c= W ) ; ::_thesis: verum end; assume A10: ( ex V being Subset of X st ( V is open & MaxADSet x c= V & V misses MaxADSet y ) or ex W being Subset of X st ( W is open & W misses MaxADSet x & MaxADSet y c= W ) ) ; ::_thesis: MaxADSet x misses MaxADSet y assume MaxADSet x meets MaxADSet y ; ::_thesis: contradiction then A11: MaxADSet x = MaxADSet y by Th22; now__::_thesis:_contradiction percases ( ex V being Subset of X st ( V is open & MaxADSet x c= V & V misses MaxADSet y ) or ex W being Subset of X st ( W is open & W misses MaxADSet x & MaxADSet y c= W ) ) by A10; suppose ex V being Subset of X st ( V is open & MaxADSet x c= V & V misses MaxADSet y ) ; ::_thesis: contradiction then consider V being Subset of X such that V is open and A12: MaxADSet x c= V and A13: V misses MaxADSet y ; V /\ (MaxADSet y) = {} by A13, XBOOLE_0:def_7; hence contradiction by A11, A12, XBOOLE_1:28; ::_thesis: verum end; suppose ex W being Subset of X st ( W is open & W misses MaxADSet x & MaxADSet y c= W ) ; ::_thesis: contradiction then consider W being Subset of X such that W is open and A14: W misses MaxADSet x and A15: MaxADSet y c= W ; W /\ (MaxADSet x) = {} by A14, XBOOLE_0:def_7; hence contradiction by A11, A15, XBOOLE_1:28; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; theorem :: TEX_4:54 for X being non empty TopSpace for x, y being Point of X holds ( MaxADSet x misses MaxADSet y iff ( ex E being Subset of X st ( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st ( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) ) proof let X be non empty TopSpace; ::_thesis: for x, y being Point of X holds ( MaxADSet x misses MaxADSet y iff ( ex E being Subset of X st ( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st ( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) ) let x, y be Point of X; ::_thesis: ( MaxADSet x misses MaxADSet y iff ( ex E being Subset of X st ( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st ( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) ) thus ( not MaxADSet x misses MaxADSet y or ex E being Subset of X st ( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st ( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) ::_thesis: ( ( ex E being Subset of X st ( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st ( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) implies MaxADSet x misses MaxADSet y ) proof assume A1: MaxADSet x misses MaxADSet y ; ::_thesis: ( ex E being Subset of X st ( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st ( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) hereby ::_thesis: verum percases ( ex V being Subset of X st ( V is open & MaxADSet x c= V & V misses MaxADSet y ) or ex W being Subset of X st ( W is open & W misses MaxADSet x & MaxADSet y c= W ) ) by A1, Th53; suppose ex V being Subset of X st ( V is open & MaxADSet x c= V & V misses MaxADSet y ) ; ::_thesis: ( ex E being Subset of X st ( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st ( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) then consider V being Subset of X such that A2: V is open and A3: MaxADSet x c= V and A4: V misses MaxADSet y ; now__::_thesis:_ex_F_being_Element_of_bool_the_carrier_of_X_st_ (_F_is_closed_&_F_misses_MaxADSet_x_&_MaxADSet_y_c=_F_) take F = V ` ; ::_thesis: ( F is closed & F misses MaxADSet x & MaxADSet y c= F ) thus F is closed by A2; ::_thesis: ( F misses MaxADSet x & MaxADSet y c= F ) thus F misses MaxADSet x by A3, SUBSET_1:24; ::_thesis: MaxADSet y c= F thus MaxADSet y c= F by A4, SUBSET_1:23; ::_thesis: verum end; hence ( ex E being Subset of X st ( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st ( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) ; ::_thesis: verum end; suppose ex W being Subset of X st ( W is open & W misses MaxADSet x & MaxADSet y c= W ) ; ::_thesis: ( ex E being Subset of X st ( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st ( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) then consider W being Subset of X such that A5: W is open and A6: W misses MaxADSet x and A7: MaxADSet y c= W ; now__::_thesis:_ex_E_being_Element_of_bool_the_carrier_of_X_st_ (_E_is_closed_&_MaxADSet_x_c=_E_&_E_misses_MaxADSet_y_) take E = W ` ; ::_thesis: ( E is closed & MaxADSet x c= E & E misses MaxADSet y ) thus E is closed by A5; ::_thesis: ( MaxADSet x c= E & E misses MaxADSet y ) thus MaxADSet x c= E by A6, SUBSET_1:23; ::_thesis: E misses MaxADSet y thus E misses MaxADSet y by A7, SUBSET_1:24; ::_thesis: verum end; hence ( ex E being Subset of X st ( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st ( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) ; ::_thesis: verum end; end; end; end; assume A8: ( ex E being Subset of X st ( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st ( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) ; ::_thesis: MaxADSet x misses MaxADSet y assume MaxADSet x meets MaxADSet y ; ::_thesis: contradiction then A9: MaxADSet x = MaxADSet y by Th22; now__::_thesis:_contradiction percases ( ex E being Subset of X st ( E is closed & MaxADSet x c= E & E misses MaxADSet y ) or ex F being Subset of X st ( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ) by A8; suppose ex E being Subset of X st ( E is closed & MaxADSet x c= E & E misses MaxADSet y ) ; ::_thesis: contradiction then consider E being Subset of X such that E is closed and A10: MaxADSet x c= E and A11: E misses MaxADSet y ; E /\ (MaxADSet y) = {} by A11, XBOOLE_0:def_7; hence contradiction by A9, A10, XBOOLE_1:28; ::_thesis: verum end; suppose ex F being Subset of X st ( F is closed & F misses MaxADSet x & MaxADSet y c= F ) ; ::_thesis: contradiction then consider F being Subset of X such that F is closed and A12: F misses MaxADSet x and A13: MaxADSet y c= F ; F /\ (MaxADSet x) = {} by A12, XBOOLE_0:def_7; hence contradiction by A9, A13, XBOOLE_1:28; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; theorem Th55: :: TEX_4:55 for X being non empty TopSpace for A being Subset of X holds MaxADSet A c= meet { G where G is Subset of X : ( G is open & A c= G ) } proof let X be non empty TopSpace; ::_thesis: for A being Subset of X holds MaxADSet A c= meet { G where G is Subset of X : ( G is open & A c= G ) } let A be Subset of X; ::_thesis: MaxADSet A c= meet { G where G is Subset of X : ( G is open & A c= G ) } set F = { G where G is Subset of X : ( G is open & A c= G ) } ; { G where G is Subset of X : ( G is open & A c= G ) } c= bool the carrier of X proof let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { G where G is Subset of X : ( G is open & A c= G ) } or C in bool the carrier of X ) assume C in { G where G is Subset of X : ( G is open & A c= G ) } ; ::_thesis: C in bool the carrier of X then ex P being Subset of X st ( C = P & P is open & A c= P ) ; hence C in bool the carrier of X ; ::_thesis: verum end; then reconsider F = { G where G is Subset of X : ( G is open & A c= G ) } as Subset-Family of X ; [#] X in F ; hence MaxADSet A c= meet { G where G is Subset of X : ( G is open & A c= G ) } by Th39; ::_thesis: verum end; theorem Th56: :: TEX_4:56 for X being non empty TopSpace for P being Subset of X st P is open holds MaxADSet P = P proof let X be non empty TopSpace; ::_thesis: for P being Subset of X st P is open holds MaxADSet P = P let P be Subset of X; ::_thesis: ( P is open implies MaxADSet P = P ) set F = { G where G is Subset of X : ( G is open & P c= G ) } ; A1: P c= MaxADSet P by Th32; assume P is open ; ::_thesis: MaxADSet P = P then P in { G where G is Subset of X : ( G is open & P c= G ) } ; then A2: meet { G where G is Subset of X : ( G is open & P c= G ) } c= P by SETFAM_1:3; MaxADSet P c= meet { G where G is Subset of X : ( G is open & P c= G ) } by Th55; then MaxADSet P c= P by A2, XBOOLE_1:1; hence MaxADSet P = P by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: TEX_4:57 for X being non empty TopSpace for A being Subset of X holds MaxADSet (Int A) = Int A by Th56; theorem Th58: :: TEX_4:58 for X being non empty TopSpace for A being Subset of X holds MaxADSet A c= meet { F where F is Subset of X : ( F is closed & A c= F ) } proof let X be non empty TopSpace; ::_thesis: for A being Subset of X holds MaxADSet A c= meet { F where F is Subset of X : ( F is closed & A c= F ) } let A be Subset of X; ::_thesis: MaxADSet A c= meet { F where F is Subset of X : ( F is closed & A c= F ) } set G = { F where F is Subset of X : ( F is closed & A c= F ) } ; { F where F is Subset of X : ( F is closed & A c= F ) } c= bool the carrier of X proof let C be set ; :: according to TARSKI:def_3 ::_thesis: ( not C in { F where F is Subset of X : ( F is closed & A c= F ) } or C in bool the carrier of X ) assume C in { F where F is Subset of X : ( F is closed & A c= F ) } ; ::_thesis: C in bool the carrier of X then ex P being Subset of X st ( C = P & P is closed & A c= P ) ; hence C in bool the carrier of X ; ::_thesis: verum end; then reconsider G = { F where F is Subset of X : ( F is closed & A c= F ) } as Subset-Family of X ; [#] X in G ; hence MaxADSet A c= meet { F where F is Subset of X : ( F is closed & A c= F ) } by Th41; ::_thesis: verum end; theorem Th59: :: TEX_4:59 for X being non empty TopSpace for A being Subset of X holds MaxADSet A c= Cl A proof let X be non empty TopSpace; ::_thesis: for A being Subset of X holds MaxADSet A c= Cl A let A be Subset of X; ::_thesis: MaxADSet A c= Cl A Cl A = meet { F where F is Subset of X : ( F is closed & A c= F ) } by Th1; hence MaxADSet A c= Cl A by Th58; ::_thesis: verum end; theorem Th60: :: TEX_4:60 for X being non empty TopSpace for P being Subset of X st P is closed holds MaxADSet P = P proof let X be non empty TopSpace; ::_thesis: for P being Subset of X st P is closed holds MaxADSet P = P let P be Subset of X; ::_thesis: ( P is closed implies MaxADSet P = P ) assume P is closed ; ::_thesis: MaxADSet P = P then A1: Cl P = P by PRE_TOPC:22; A2: P c= MaxADSet P by Th32; MaxADSet P c= Cl P by Th59; hence MaxADSet P = P by A1, A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: TEX_4:61 for X being non empty TopSpace for A being Subset of X holds MaxADSet (Cl A) = Cl A by Th60; theorem :: TEX_4:62 for X being non empty TopSpace for A being Subset of X holds Cl (MaxADSet A) = Cl A proof let X be non empty TopSpace; ::_thesis: for A being Subset of X holds Cl (MaxADSet A) = Cl A let A be Subset of X; ::_thesis: Cl (MaxADSet A) = Cl A A1: Cl (MaxADSet A) c= Cl A by Th59, TOPS_1:5; Cl A c= Cl (MaxADSet A) by Th32, PRE_TOPC:19; hence Cl (MaxADSet A) = Cl A by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: TEX_4:63 for X being non empty TopSpace for A, B being Subset of X st MaxADSet A = MaxADSet B holds Cl A = Cl B proof let X be non empty TopSpace; ::_thesis: for A, B being Subset of X st MaxADSet A = MaxADSet B holds Cl A = Cl B let A, B be Subset of X; ::_thesis: ( MaxADSet A = MaxADSet B implies Cl A = Cl B ) A1: MaxADSet A c= Cl A by Th59; A2: MaxADSet B c= Cl B by Th59; assume A3: MaxADSet A = MaxADSet B ; ::_thesis: Cl A = Cl B then A c= MaxADSet B by Th32; then A c= Cl B by A2, XBOOLE_1:1; then A4: Cl A c= Cl B by TOPS_1:5; B c= MaxADSet A by A3, Th32; then B c= Cl A by A1, XBOOLE_1:1; then Cl B c= Cl A by TOPS_1:5; hence Cl A = Cl B by A4, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: TEX_4:64 for X being non empty TopSpace for P, Q being Subset of X st ( P is closed or Q is closed ) holds MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q) proof let X be non empty TopSpace; ::_thesis: for P, Q being Subset of X st ( P is closed or Q is closed ) holds MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q) let P, Q be Subset of X; ::_thesis: ( ( P is closed or Q is closed ) implies MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q) ) assume A1: ( P is closed or Q is closed ) ; ::_thesis: MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q) A2: (MaxADSet P) /\ (MaxADSet Q) c= MaxADSet (P /\ Q) proof assume not (MaxADSet P) /\ (MaxADSet Q) c= MaxADSet (P /\ Q) ; ::_thesis: contradiction then consider x being set such that A3: x in (MaxADSet P) /\ (MaxADSet Q) and A4: not x in MaxADSet (P /\ Q) by TARSKI:def_3; reconsider x = x as Point of X by A3; now__::_thesis:_contradiction percases ( P is closed or Q is closed ) by A1; supposeA5: P is closed ; ::_thesis: contradiction then P = MaxADSet P by Th60; then x in P by A3, XBOOLE_0:def_4; then A6: MaxADSet x c= P by A5, Th23; A7: P /\ Q c= MaxADSet (P /\ Q) by Th32; x in MaxADSet Q by A3, XBOOLE_0:def_4; then consider D being set such that A8: x in D and A9: D in { (MaxADSet b) where b is Point of X : b in Q } by TARSKI:def_4; consider b being Point of X such that A10: D = MaxADSet b and A11: b in Q by A9; {b} c= MaxADSet b by Th12; then A12: b in MaxADSet b by ZFMISC_1:31; MaxADSet x = MaxADSet b by A8, A10, Th21; then b in P /\ Q by A6, A11, A12, XBOOLE_0:def_4; then MaxADSet b meets MaxADSet (P /\ Q) by A12, A7, XBOOLE_0:3; then MaxADSet b c= MaxADSet (P /\ Q) by Th30; hence contradiction by A4, A8, A10; ::_thesis: verum end; supposeA13: Q is closed ; ::_thesis: contradiction then Q = MaxADSet Q by Th60; then x in Q by A3, XBOOLE_0:def_4; then A14: MaxADSet x c= Q by A13, Th23; A15: P /\ Q c= MaxADSet (P /\ Q) by Th32; x in MaxADSet P by A3, XBOOLE_0:def_4; then consider D being set such that A16: x in D and A17: D in { (MaxADSet b) where b is Point of X : b in P } by TARSKI:def_4; consider b being Point of X such that A18: D = MaxADSet b and A19: b in P by A17; {b} c= MaxADSet b by Th12; then A20: b in MaxADSet b by ZFMISC_1:31; MaxADSet x = MaxADSet b by A16, A18, Th21; then b in P /\ Q by A14, A19, A20, XBOOLE_0:def_4; then MaxADSet b meets MaxADSet (P /\ Q) by A20, A15, XBOOLE_0:3; then MaxADSet b c= MaxADSet (P /\ Q) by Th30; hence contradiction by A4, A16, A18; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; MaxADSet (P /\ Q) c= (MaxADSet P) /\ (MaxADSet Q) by Th37; hence MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q) by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: TEX_4:65 for X being non empty TopSpace for P, Q being Subset of X st ( P is open or Q is open ) holds MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q) proof let X be non empty TopSpace; ::_thesis: for P, Q being Subset of X st ( P is open or Q is open ) holds MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q) let P, Q be Subset of X; ::_thesis: ( ( P is open or Q is open ) implies MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q) ) assume A1: ( P is open or Q is open ) ; ::_thesis: MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q) A2: (MaxADSet P) /\ (MaxADSet Q) c= MaxADSet (P /\ Q) proof assume not (MaxADSet P) /\ (MaxADSet Q) c= MaxADSet (P /\ Q) ; ::_thesis: contradiction then consider x being set such that A3: x in (MaxADSet P) /\ (MaxADSet Q) and A4: not x in MaxADSet (P /\ Q) by TARSKI:def_3; reconsider x = x as Point of X by A3; now__::_thesis:_contradiction percases ( P is open or Q is open ) by A1; supposeA5: P is open ; ::_thesis: contradiction then P = MaxADSet P by Th56; then x in P by A3, XBOOLE_0:def_4; then A6: MaxADSet x c= P by A5, Th24; A7: P /\ Q c= MaxADSet (P /\ Q) by Th32; x in MaxADSet Q by A3, XBOOLE_0:def_4; then consider D being set such that A8: x in D and A9: D in { (MaxADSet b) where b is Point of X : b in Q } by TARSKI:def_4; consider b being Point of X such that A10: D = MaxADSet b and A11: b in Q by A9; {b} c= MaxADSet b by Th12; then A12: b in MaxADSet b by ZFMISC_1:31; MaxADSet x = MaxADSet b by A8, A10, Th21; then b in P /\ Q by A6, A11, A12, XBOOLE_0:def_4; then MaxADSet b meets MaxADSet (P /\ Q) by A12, A7, XBOOLE_0:3; then MaxADSet b c= MaxADSet (P /\ Q) by Th30; hence contradiction by A4, A8, A10; ::_thesis: verum end; supposeA13: Q is open ; ::_thesis: contradiction then Q = MaxADSet Q by Th56; then x in Q by A3, XBOOLE_0:def_4; then A14: MaxADSet x c= Q by A13, Th24; A15: P /\ Q c= MaxADSet (P /\ Q) by Th32; x in MaxADSet P by A3, XBOOLE_0:def_4; then consider D being set such that A16: x in D and A17: D in { (MaxADSet b) where b is Point of X : b in P } by TARSKI:def_4; consider b being Point of X such that A18: D = MaxADSet b and A19: b in P by A17; {b} c= MaxADSet b by Th12; then A20: b in MaxADSet b by ZFMISC_1:31; MaxADSet x = MaxADSet b by A16, A18, Th21; then b in P /\ Q by A14, A19, A20, XBOOLE_0:def_4; then MaxADSet b meets MaxADSet (P /\ Q) by A20, A15, XBOOLE_0:3; then MaxADSet b c= MaxADSet (P /\ Q) by Th30; hence contradiction by A4, A16, A18; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; MaxADSet (P /\ Q) c= (MaxADSet P) /\ (MaxADSet Q) by Th37; hence MaxADSet (P /\ Q) = (MaxADSet P) /\ (MaxADSet Q) by A2, XBOOLE_0:def_10; ::_thesis: verum end; begin theorem Th66: :: TEX_4:66 for Y being non empty TopStruct for Y0 being SubSpace of Y for A being Subset of Y st A = the carrier of Y0 & Y0 is anti-discrete holds A is anti-discrete proof let Y be non empty TopStruct ; ::_thesis: for Y0 being SubSpace of Y for A being Subset of Y st A = the carrier of Y0 & Y0 is anti-discrete holds A is anti-discrete let Y0 be SubSpace of Y; ::_thesis: for A being Subset of Y st A = the carrier of Y0 & Y0 is anti-discrete holds A is anti-discrete let A be Subset of Y; ::_thesis: ( A = the carrier of Y0 & Y0 is anti-discrete implies A is anti-discrete ) assume A1: A = the carrier of Y0 ; ::_thesis: ( not Y0 is anti-discrete or A is anti-discrete ) assume Y0 is anti-discrete ; ::_thesis: A is anti-discrete then A2: the topology of Y0 = {{}, the carrier of Y0} by TDLAT_3:def_2; now__::_thesis:_for_G_being_Subset_of_Y_holds_ (_not_G_is_open_or_A_misses_G_or_A_c=_G_) let G be Subset of Y; ::_thesis: ( not G is open or A misses G or A c= G ) reconsider H = A /\ G as Subset of Y0 by A1, XBOOLE_1:17; assume A3: G is open ; ::_thesis: ( A misses G or A c= G ) now__::_thesis:_ex_G_being_Subset_of_Y_st_ (_G_in_the_topology_of_Y_&_H_=_G_/\_([#]_Y0)_) take G = G; ::_thesis: ( G in the topology of Y & H = G /\ ([#] Y0) ) thus G in the topology of Y by A3, PRE_TOPC:def_2; ::_thesis: H = G /\ ([#] Y0) thus H = G /\ ([#] Y0) by A1; ::_thesis: verum end; then H in the topology of Y0 by PRE_TOPC:def_4; then ( A /\ G = {} or A /\ G = the carrier of Y0 ) by A2, TARSKI:def_2; hence ( A misses G or A c= G ) by A1, XBOOLE_0:def_7, XBOOLE_1:17; ::_thesis: verum end; hence A is anti-discrete by Def3; ::_thesis: verum end; theorem Th67: :: TEX_4:67 for Y being non empty TopStruct for Y0 being SubSpace of Y st Y0 is TopSpace-like holds for A being Subset of Y st A = the carrier of Y0 & A is anti-discrete holds Y0 is anti-discrete proof let Y be non empty TopStruct ; ::_thesis: for Y0 being SubSpace of Y st Y0 is TopSpace-like holds for A being Subset of Y st A = the carrier of Y0 & A is anti-discrete holds Y0 is anti-discrete let Y0 be SubSpace of Y; ::_thesis: ( Y0 is TopSpace-like implies for A being Subset of Y st A = the carrier of Y0 & A is anti-discrete holds Y0 is anti-discrete ) assume A1: Y0 is TopSpace-like ; ::_thesis: for A being Subset of Y st A = the carrier of Y0 & A is anti-discrete holds Y0 is anti-discrete then A2: the carrier of Y0 in the topology of Y0 by PRE_TOPC:def_1; let A be Subset of Y; ::_thesis: ( A = the carrier of Y0 & A is anti-discrete implies Y0 is anti-discrete ) assume A3: A = the carrier of Y0 ; ::_thesis: ( not A is anti-discrete or Y0 is anti-discrete ) assume A4: A is anti-discrete ; ::_thesis: Y0 is anti-discrete now__::_thesis:_for_D_being_set_st_D_in_the_topology_of_Y0_holds_ D_in_{{},_the_carrier_of_Y0} let D be set ; ::_thesis: ( D in the topology of Y0 implies D in {{}, the carrier of Y0} ) assume A5: D in the topology of Y0 ; ::_thesis: D in {{}, the carrier of Y0} then reconsider C = D as Subset of Y0 ; consider E being Subset of Y such that A6: E in the topology of Y and A7: C = E /\ ([#] Y0) by A5, PRE_TOPC:def_4; reconsider E = E as Subset of Y ; A8: E is open by A6, PRE_TOPC:def_2; now__::_thesis:_(_C_=_{}_or_C_=_A_) percases ( A misses E or A c= E ) by A4, A8, Def3; suppose A misses E ; ::_thesis: ( C = {} or C = A ) hence ( C = {} or C = A ) by A3, A7, XBOOLE_0:def_7; ::_thesis: verum end; suppose A c= E ; ::_thesis: ( C = {} or C = A ) hence ( C = {} or C = A ) by A3, A7, XBOOLE_1:28; ::_thesis: verum end; end; end; hence D in {{}, the carrier of Y0} by A3, TARSKI:def_2; ::_thesis: verum end; then A9: the topology of Y0 c= {{}, the carrier of Y0} by TARSKI:def_3; {} in the topology of Y0 by A1, PRE_TOPC:1; then {{}, the carrier of Y0} c= the topology of Y0 by A2, ZFMISC_1:32; then the topology of Y0 = {{}, the carrier of Y0} by A9, XBOOLE_0:def_10; hence Y0 is anti-discrete by TDLAT_3:def_2; ::_thesis: verum end; theorem :: TEX_4:68 for X being non empty TopSpace for Y0 being non empty SubSpace of X st ( for X0 being open SubSpace of X holds ( Y0 misses X0 or Y0 is SubSpace of X0 ) ) holds Y0 is anti-discrete proof let X be non empty TopSpace; ::_thesis: for Y0 being non empty SubSpace of X st ( for X0 being open SubSpace of X holds ( Y0 misses X0 or Y0 is SubSpace of X0 ) ) holds Y0 is anti-discrete let Y0 be non empty SubSpace of X; ::_thesis: ( ( for X0 being open SubSpace of X holds ( Y0 misses X0 or Y0 is SubSpace of X0 ) ) implies Y0 is anti-discrete ) reconsider A = the carrier of Y0 as Subset of X by TSEP_1:1; assume A1: for X0 being open SubSpace of X holds ( Y0 misses X0 or Y0 is SubSpace of X0 ) ; ::_thesis: Y0 is anti-discrete now__::_thesis:_for_G_being_Subset_of_X_holds_ (_not_G_is_open_or_A_misses_G_or_A_c=_G_) let G be Subset of X; ::_thesis: ( not G is open or A misses G or A c= G ) assume A2: G is open ; ::_thesis: ( A misses G or A c= G ) now__::_thesis:_(_A_misses_G_or_A_c=_G_) percases ( G is empty or not G is empty ) ; suppose G is empty ; ::_thesis: ( A misses G or A c= G ) hence ( A misses G or A c= G ) by XBOOLE_1:65; ::_thesis: verum end; suppose not G is empty ; ::_thesis: ( A misses G or A c= G ) then consider X0 being non empty strict open SubSpace of X such that A3: G = the carrier of X0 by A2, TSEP_1:20; ( Y0 misses X0 or Y0 is SubSpace of X0 ) by A1; hence ( A misses G or A c= G ) by A3, TSEP_1:4, TSEP_1:def_3; ::_thesis: verum end; end; end; hence ( A misses G or A c= G ) ; ::_thesis: verum end; then A is anti-discrete by Def3; hence Y0 is anti-discrete by Th67; ::_thesis: verum end; theorem :: TEX_4:69 for X being non empty TopSpace for Y0 being non empty SubSpace of X st ( for X0 being closed SubSpace of X holds ( Y0 misses X0 or Y0 is SubSpace of X0 ) ) holds Y0 is anti-discrete proof let X be non empty TopSpace; ::_thesis: for Y0 being non empty SubSpace of X st ( for X0 being closed SubSpace of X holds ( Y0 misses X0 or Y0 is SubSpace of X0 ) ) holds Y0 is anti-discrete let Y0 be non empty SubSpace of X; ::_thesis: ( ( for X0 being closed SubSpace of X holds ( Y0 misses X0 or Y0 is SubSpace of X0 ) ) implies Y0 is anti-discrete ) reconsider A = the carrier of Y0 as Subset of X by TSEP_1:1; assume A1: for X0 being closed SubSpace of X holds ( Y0 misses X0 or Y0 is SubSpace of X0 ) ; ::_thesis: Y0 is anti-discrete now__::_thesis:_for_G_being_Subset_of_X_holds_ (_not_G_is_closed_or_A_misses_G_or_A_c=_G_) let G be Subset of X; ::_thesis: ( not G is closed or A misses G or A c= G ) assume A2: G is closed ; ::_thesis: ( A misses G or A c= G ) now__::_thesis:_(_A_misses_G_or_A_c=_G_) percases ( G is empty or not G is empty ) ; suppose G is empty ; ::_thesis: ( A misses G or A c= G ) hence ( A misses G or A c= G ) by XBOOLE_1:65; ::_thesis: verum end; suppose not G is empty ; ::_thesis: ( A misses G or A c= G ) then consider X0 being non empty strict closed SubSpace of X such that A3: G = the carrier of X0 by A2, TSEP_1:15; ( Y0 misses X0 or Y0 is SubSpace of X0 ) by A1; hence ( A misses G or A c= G ) by A3, TSEP_1:4, TSEP_1:def_3; ::_thesis: verum end; end; end; hence ( A misses G or A c= G ) ; ::_thesis: verum end; then A is anti-discrete by Def4; hence Y0 is anti-discrete by Th67; ::_thesis: verum end; theorem :: TEX_4:70 for X being non empty TopSpace for Y0 being anti-discrete SubSpace of X for X0 being open SubSpace of X holds ( Y0 misses X0 or Y0 is SubSpace of X0 ) proof let X be non empty TopSpace; ::_thesis: for Y0 being anti-discrete SubSpace of X for X0 being open SubSpace of X holds ( Y0 misses X0 or Y0 is SubSpace of X0 ) let Y0 be anti-discrete SubSpace of X; ::_thesis: for X0 being open SubSpace of X holds ( Y0 misses X0 or Y0 is SubSpace of X0 ) reconsider A = the carrier of Y0 as Subset of X by TSEP_1:1; let X0 be open SubSpace of X; ::_thesis: ( Y0 misses X0 or Y0 is SubSpace of X0 ) reconsider G = the carrier of X0 as Subset of X by TSEP_1:1; A1: G is open by TSEP_1:16; A is anti-discrete by Th66; then ( A misses G or A c= G ) by A1, Def3; hence ( Y0 misses X0 or Y0 is SubSpace of X0 ) by TSEP_1:4, TSEP_1:def_3; ::_thesis: verum end; theorem :: TEX_4:71 for X being non empty TopSpace for Y0 being anti-discrete SubSpace of X for X0 being closed SubSpace of X holds ( Y0 misses X0 or Y0 is SubSpace of X0 ) proof let X be non empty TopSpace; ::_thesis: for Y0 being anti-discrete SubSpace of X for X0 being closed SubSpace of X holds ( Y0 misses X0 or Y0 is SubSpace of X0 ) let Y0 be anti-discrete SubSpace of X; ::_thesis: for X0 being closed SubSpace of X holds ( Y0 misses X0 or Y0 is SubSpace of X0 ) reconsider A = the carrier of Y0 as Subset of X by TSEP_1:1; let X0 be closed SubSpace of X; ::_thesis: ( Y0 misses X0 or Y0 is SubSpace of X0 ) reconsider G = the carrier of X0 as Subset of X by TSEP_1:1; A1: G is closed by TSEP_1:11; A is anti-discrete by Th66; then ( A misses G or A c= G ) by A1, Def4; hence ( Y0 misses X0 or Y0 is SubSpace of X0 ) by TSEP_1:4, TSEP_1:def_3; ::_thesis: verum end; definition let Y be non empty TopStruct ; let IT be SubSpace of Y; attrIT is maximal_anti-discrete means :Def16: :: TEX_4:def 16 ( IT is anti-discrete & ( for Y0 being SubSpace of Y st Y0 is anti-discrete & the carrier of IT c= the carrier of Y0 holds the carrier of IT = the carrier of Y0 ) ); end; :: deftheorem Def16 defines maximal_anti-discrete TEX_4:def_16_:_ for Y being non empty TopStruct for IT being SubSpace of Y holds ( IT is maximal_anti-discrete iff ( IT is anti-discrete & ( for Y0 being SubSpace of Y st Y0 is anti-discrete & the carrier of IT c= the carrier of Y0 holds the carrier of IT = the carrier of Y0 ) ) ); registration let Y be non empty TopStruct ; cluster maximal_anti-discrete -> anti-discrete for SubSpace of Y; coherence for b1 being SubSpace of Y st b1 is maximal_anti-discrete holds b1 is anti-discrete by Def16; cluster non anti-discrete -> non maximal_anti-discrete for SubSpace of Y; coherence for b1 being SubSpace of Y st not b1 is anti-discrete holds not b1 is maximal_anti-discrete ; end; theorem Th72: :: TEX_4:72 for X being non empty TopSpace for Y0 being non empty SubSpace of X for A being Subset of X st A = the carrier of Y0 holds ( Y0 is maximal_anti-discrete iff A is maximal_anti-discrete ) proof let X be non empty TopSpace; ::_thesis: for Y0 being non empty SubSpace of X for A being Subset of X st A = the carrier of Y0 holds ( Y0 is maximal_anti-discrete iff A is maximal_anti-discrete ) let Y0 be non empty SubSpace of X; ::_thesis: for A being Subset of X st A = the carrier of Y0 holds ( Y0 is maximal_anti-discrete iff A is maximal_anti-discrete ) let A be Subset of X; ::_thesis: ( A = the carrier of Y0 implies ( Y0 is maximal_anti-discrete iff A is maximal_anti-discrete ) ) assume A1: A = the carrier of Y0 ; ::_thesis: ( Y0 is maximal_anti-discrete iff A is maximal_anti-discrete ) thus ( Y0 is maximal_anti-discrete implies A is maximal_anti-discrete ) ::_thesis: ( A is maximal_anti-discrete implies Y0 is maximal_anti-discrete ) proof assume A2: Y0 is maximal_anti-discrete ; ::_thesis: A is maximal_anti-discrete A3: now__::_thesis:_for_D_being_Subset_of_X_st_D_is_anti-discrete_&_A_c=_D_holds_ A_=_D let D be Subset of X; ::_thesis: ( D is anti-discrete & A c= D implies A = D ) assume A4: D is anti-discrete ; ::_thesis: ( A c= D implies A = D ) assume A5: A c= D ; ::_thesis: A = D then D <> {} by A1; then consider X0 being non empty strict SubSpace of X such that A6: D = the carrier of X0 by TSEP_1:10; X0 is anti-discrete by A4, A6, Th67; hence A = D by A1, A2, A5, A6, Def16; ::_thesis: verum end; A is anti-discrete by A1, A2, Th66; hence A is maximal_anti-discrete by A3, Def7; ::_thesis: verum end; assume A7: A is maximal_anti-discrete ; ::_thesis: Y0 is maximal_anti-discrete A8: now__::_thesis:_for_X0_being_SubSpace_of_X_st_X0_is_anti-discrete_&_the_carrier_of_Y0_c=_the_carrier_of_X0_holds_ the_carrier_of_Y0_=_the_carrier_of_X0 let X0 be SubSpace of X; ::_thesis: ( X0 is anti-discrete & the carrier of Y0 c= the carrier of X0 implies the carrier of Y0 = the carrier of X0 ) reconsider D = the carrier of X0 as Subset of X by TSEP_1:1; assume X0 is anti-discrete ; ::_thesis: ( the carrier of Y0 c= the carrier of X0 implies the carrier of Y0 = the carrier of X0 ) then A9: D is anti-discrete by Th66; assume the carrier of Y0 c= the carrier of X0 ; ::_thesis: the carrier of Y0 = the carrier of X0 hence the carrier of Y0 = the carrier of X0 by A1, A7, A9, Def7; ::_thesis: verum end; A is anti-discrete by A7, Def7; then Y0 is anti-discrete by A1, Th67; hence Y0 is maximal_anti-discrete by A8, Def16; ::_thesis: verum end; registration let X be non empty TopSpace; cluster non empty open anti-discrete -> non empty maximal_anti-discrete for SubSpace of X; coherence for b1 being non empty SubSpace of X st b1 is open & b1 is anti-discrete holds b1 is maximal_anti-discrete proof let X0 be non empty SubSpace of X; ::_thesis: ( X0 is open & X0 is anti-discrete implies X0 is maximal_anti-discrete ) reconsider A = the carrier of X0 as Subset of X by TSEP_1:1; assume X0 is open ; ::_thesis: ( not X0 is anti-discrete or X0 is maximal_anti-discrete ) then A1: A is open by TSEP_1:16; assume X0 is anti-discrete ; ::_thesis: X0 is maximal_anti-discrete then A is anti-discrete by Th66; then A is maximal_anti-discrete by A1, Th16; hence X0 is maximal_anti-discrete by Th72; ::_thesis: verum end; cluster non empty open non maximal_anti-discrete -> non empty non anti-discrete for SubSpace of X; coherence for b1 being non empty SubSpace of X st b1 is open & not b1 is maximal_anti-discrete holds not b1 is anti-discrete ; cluster non empty anti-discrete non maximal_anti-discrete -> non empty non open for SubSpace of X; coherence for b1 being non empty SubSpace of X st b1 is anti-discrete & not b1 is maximal_anti-discrete holds not b1 is open ; cluster non empty closed anti-discrete -> non empty maximal_anti-discrete for SubSpace of X; coherence for b1 being non empty SubSpace of X st b1 is closed & b1 is anti-discrete holds b1 is maximal_anti-discrete proof let X0 be non empty SubSpace of X; ::_thesis: ( X0 is closed & X0 is anti-discrete implies X0 is maximal_anti-discrete ) reconsider A = the carrier of X0 as Subset of X by TSEP_1:1; assume X0 is closed ; ::_thesis: ( not X0 is anti-discrete or X0 is maximal_anti-discrete ) then A2: A is closed by TSEP_1:11; assume X0 is anti-discrete ; ::_thesis: X0 is maximal_anti-discrete then A is anti-discrete by Th66; then A is maximal_anti-discrete by A2, Th17; hence X0 is maximal_anti-discrete by Th72; ::_thesis: verum end; cluster non empty closed non maximal_anti-discrete -> non empty non anti-discrete for SubSpace of X; coherence for b1 being non empty SubSpace of X st b1 is closed & not b1 is maximal_anti-discrete holds not b1 is anti-discrete ; cluster non empty anti-discrete non maximal_anti-discrete -> non empty non closed for SubSpace of X; coherence for b1 being non empty SubSpace of X st b1 is anti-discrete & not b1 is maximal_anti-discrete holds not b1 is closed ; end; definition let Y be TopStruct ; let x be Point of Y; func MaxADSspace x -> strict SubSpace of Y means :Def17: :: TEX_4:def 17 the carrier of it = MaxADSet x; existence ex b1 being strict SubSpace of Y st the carrier of b1 = MaxADSet x proof set D = MaxADSet x; set Y0 = Y | (MaxADSet x); take Y | (MaxADSet x) ; ::_thesis: the carrier of (Y | (MaxADSet x)) = MaxADSet x MaxADSet x = [#] (Y | (MaxADSet x)) by PRE_TOPC:def_5; hence the carrier of (Y | (MaxADSet x)) = MaxADSet x ; ::_thesis: verum end; uniqueness for b1, b2 being strict SubSpace of Y st the carrier of b1 = MaxADSet x & the carrier of b2 = MaxADSet x holds b1 = b2 proof let Y1, Y2 be strict SubSpace of Y; ::_thesis: ( the carrier of Y1 = MaxADSet x & the carrier of Y2 = MaxADSet x implies Y1 = Y2 ) assume that A1: the carrier of Y1 = MaxADSet x and A2: the carrier of Y2 = MaxADSet x ; ::_thesis: Y1 = Y2 set A1 = the carrier of Y1; set A2 = the carrier of Y2; A3: the carrier of Y2 = [#] Y2 ; A4: the carrier of Y1 = [#] Y1 ; then the carrier of Y1 c= [#] Y by PRE_TOPC:def_4; then reconsider A1 = the carrier of Y1 as Subset of Y ; Y1 = Y | A1 by A4, PRE_TOPC:def_5; hence Y1 = Y2 by A1, A2, A3, PRE_TOPC:def_5; ::_thesis: verum end; end; :: deftheorem Def17 defines MaxADSspace TEX_4:def_17_:_ for Y being TopStruct for x being Point of Y for b3 being strict SubSpace of Y holds ( b3 = MaxADSspace x iff the carrier of b3 = MaxADSet x ); registration let Y be non empty TopStruct ; let x be Point of Y; cluster MaxADSspace x -> non empty strict ; coherence not MaxADSspace x is empty proof the carrier of (MaxADSspace x) = MaxADSet x by Def17; hence not the carrier of (MaxADSspace x) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum end; end; Lm2: for Y being non empty TopStruct for X1, X2 being SubSpace of Y st the carrier of X1 c= the carrier of X2 holds X1 is SubSpace of X2 proof let Y be non empty TopStruct ; ::_thesis: for X1, X2 being SubSpace of Y st the carrier of X1 c= the carrier of X2 holds X1 is SubSpace of X2 let X1, X2 be SubSpace of Y; ::_thesis: ( the carrier of X1 c= the carrier of X2 implies X1 is SubSpace of X2 ) set A1 = the carrier of X1; set A2 = the carrier of X2; A1: the carrier of X1 = [#] X1 ; assume A2: the carrier of X1 c= the carrier of X2 ; ::_thesis: X1 is SubSpace of X2 A3: the carrier of X2 = [#] X2 ; for P being Subset of X1 holds ( P in the topology of X1 iff ex Q being Subset of X2 st ( Q in the topology of X2 & P = Q /\ the carrier of X1 ) ) proof let P be Subset of X1; ::_thesis: ( P in the topology of X1 iff ex Q being Subset of X2 st ( Q in the topology of X2 & P = Q /\ the carrier of X1 ) ) thus ( P in the topology of X1 implies ex Q being Subset of X2 st ( Q in the topology of X2 & P = Q /\ the carrier of X1 ) ) ::_thesis: ( ex Q being Subset of X2 st ( Q in the topology of X2 & P = Q /\ the carrier of X1 ) implies P in the topology of X1 ) proof assume P in the topology of X1 ; ::_thesis: ex Q being Subset of X2 st ( Q in the topology of X2 & P = Q /\ the carrier of X1 ) then consider R being Subset of Y such that A4: R in the topology of Y and A5: P = R /\ the carrier of X1 by A1, PRE_TOPC:def_4; reconsider Q = R /\ the carrier of X2 as Subset of X2 by XBOOLE_1:17; take Q ; ::_thesis: ( Q in the topology of X2 & P = Q /\ the carrier of X1 ) thus Q in the topology of X2 by A3, A4, PRE_TOPC:def_4; ::_thesis: P = Q /\ the carrier of X1 Q /\ the carrier of X1 = R /\ ( the carrier of X2 /\ the carrier of X1) by XBOOLE_1:16 .= R /\ the carrier of X1 by A2, XBOOLE_1:28 ; hence P = Q /\ the carrier of X1 by A5; ::_thesis: verum end; given Q being Subset of X2 such that A6: Q in the topology of X2 and A7: P = Q /\ the carrier of X1 ; ::_thesis: P in the topology of X1 consider R being Subset of Y such that A8: R in the topology of Y and A9: Q = R /\ ([#] X2) by A6, PRE_TOPC:def_4; P = R /\ ( the carrier of X2 /\ the carrier of X1) by A7, A9, XBOOLE_1:16 .= R /\ the carrier of X1 by A2, XBOOLE_1:28 ; hence P in the topology of X1 by A1, A8, PRE_TOPC:def_4; ::_thesis: verum end; hence X1 is SubSpace of X2 by A1, A3, A2, PRE_TOPC:def_4; ::_thesis: verum end; theorem :: TEX_4:73 for Y being non empty TopStruct for x being Point of Y holds Sspace x is SubSpace of MaxADSspace x proof let Y be non empty TopStruct ; ::_thesis: for x being Point of Y holds Sspace x is SubSpace of MaxADSspace x let x be Point of Y; ::_thesis: Sspace x is SubSpace of MaxADSspace x A1: the carrier of (Sspace x) = {x} by TEX_2:def_2; the carrier of (MaxADSspace x) = MaxADSet x by Def17; hence Sspace x is SubSpace of MaxADSspace x by A1, Lm2, Th12; ::_thesis: verum end; theorem :: TEX_4:74 for Y being non empty TopStruct for x, y being Point of Y holds ( y is Point of (MaxADSspace x) iff TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) = TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) ) proof let Y be non empty TopStruct ; ::_thesis: for x, y being Point of Y holds ( y is Point of (MaxADSspace x) iff TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) = TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) ) let x, y be Point of Y; ::_thesis: ( y is Point of (MaxADSspace x) iff TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) = TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) ) A1: the carrier of (MaxADSspace x) = MaxADSet x by Def17; thus ( y is Point of (MaxADSspace x) implies TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) = TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) ) ::_thesis: ( TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) = TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) implies y is Point of (MaxADSspace x) ) proof assume y is Point of (MaxADSspace x) ; ::_thesis: TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) = TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) then MaxADSet y = MaxADSet x by A1, Th21; hence TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) = TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) by A1, Def17; ::_thesis: verum end; assume A2: TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) = TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) ; ::_thesis: y is Point of (MaxADSspace x) the carrier of (MaxADSspace y) = MaxADSet y by Def17; hence y is Point of (MaxADSspace x) by A2, Th21; ::_thesis: verum end; theorem :: TEX_4:75 for Y being non empty TopStruct for x, y being Point of Y holds ( the carrier of (MaxADSspace x) misses the carrier of (MaxADSspace y) or TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) ) proof let Y be non empty TopStruct ; ::_thesis: for x, y being Point of Y holds ( the carrier of (MaxADSspace x) misses the carrier of (MaxADSspace y) or TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) ) let x, y be Point of Y; ::_thesis: ( the carrier of (MaxADSspace x) misses the carrier of (MaxADSspace y) or TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) ) assume A1: the carrier of (MaxADSspace x) meets the carrier of (MaxADSspace y) ; ::_thesis: TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) A2: the carrier of (MaxADSspace y) = MaxADSet y by Def17; the carrier of (MaxADSspace x) = MaxADSet x by Def17; hence TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace y), the topology of (MaxADSspace y) #) by A2, A1, Th22, TSEP_1:5; ::_thesis: verum end; registration let X be non empty TopSpace; cluster strict TopSpace-like maximal_anti-discrete for SubSpace of X; existence ex b1 being SubSpace of X st ( b1 is maximal_anti-discrete & b1 is strict ) proof consider a being set such that A1: a in the carrier of X by XBOOLE_0:def_1; reconsider a = a as Point of X by A1; consider X0 being non empty strict SubSpace of X such that A2: MaxADSet a = the carrier of X0 by TSEP_1:10; take X0 ; ::_thesis: ( X0 is maximal_anti-discrete & X0 is strict ) MaxADSet a is maximal_anti-discrete by Th20; hence ( X0 is maximal_anti-discrete & X0 is strict ) by A2, Th72; ::_thesis: verum end; end; registration let X be non empty TopSpace; let x be Point of X; cluster MaxADSspace x -> strict maximal_anti-discrete ; coherence MaxADSspace x is maximal_anti-discrete proof A1: MaxADSet x is maximal_anti-discrete by Th20; MaxADSet x = the carrier of (MaxADSspace x) by Def17; hence MaxADSspace x is maximal_anti-discrete by A1, Th72; ::_thesis: verum end; end; theorem :: TEX_4:76 for X being non empty TopSpace for X0 being non empty closed SubSpace of X for x being Point of X st x is Point of X0 holds MaxADSspace x is SubSpace of X0 proof let X be non empty TopSpace; ::_thesis: for X0 being non empty closed SubSpace of X for x being Point of X st x is Point of X0 holds MaxADSspace x is SubSpace of X0 let X0 be non empty closed SubSpace of X; ::_thesis: for x being Point of X st x is Point of X0 holds MaxADSspace x is SubSpace of X0 let x be Point of X; ::_thesis: ( x is Point of X0 implies MaxADSspace x is SubSpace of X0 ) reconsider A = the carrier of X0 as Subset of X by TSEP_1:1; A1: A is closed by TSEP_1:11; assume x is Point of X0 ; ::_thesis: MaxADSspace x is SubSpace of X0 then MaxADSet x c= A by A1, Th23; then the carrier of (MaxADSspace x) c= the carrier of X0 by Def17; hence MaxADSspace x is SubSpace of X0 by Lm2; ::_thesis: verum end; theorem :: TEX_4:77 for X being non empty TopSpace for X0 being non empty open SubSpace of X for x being Point of X st x is Point of X0 holds MaxADSspace x is SubSpace of X0 proof let X be non empty TopSpace; ::_thesis: for X0 being non empty open SubSpace of X for x being Point of X st x is Point of X0 holds MaxADSspace x is SubSpace of X0 let X0 be non empty open SubSpace of X; ::_thesis: for x being Point of X st x is Point of X0 holds MaxADSspace x is SubSpace of X0 let x be Point of X; ::_thesis: ( x is Point of X0 implies MaxADSspace x is SubSpace of X0 ) reconsider A = the carrier of X0 as Subset of X by TSEP_1:1; A1: A is open by TSEP_1:16; assume x is Point of X0 ; ::_thesis: MaxADSspace x is SubSpace of X0 then MaxADSet x c= A by A1, Th24; then the carrier of (MaxADSspace x) c= the carrier of X0 by Def17; hence MaxADSspace x is SubSpace of X0 by Lm2; ::_thesis: verum end; theorem :: TEX_4:78 for X being non empty TopSpace for x being Point of X st Cl {x} = {x} holds Sspace x is maximal_anti-discrete proof let X be non empty TopSpace; ::_thesis: for x being Point of X st Cl {x} = {x} holds Sspace x is maximal_anti-discrete let x be Point of X; ::_thesis: ( Cl {x} = {x} implies Sspace x is maximal_anti-discrete ) assume Cl {x} = {x} ; ::_thesis: Sspace x is maximal_anti-discrete then A1: {x} is maximal_anti-discrete by Th45; the carrier of (Sspace x) = {x} by TEX_2:def_2; hence Sspace x is maximal_anti-discrete by A1, Th72; ::_thesis: verum end; notation let Y be TopStruct ; let A be Subset of Y; synonym Sspace A for Y | A; end; Lm3: for Y being TopStruct for A being Subset of Y holds the carrier of (Y | A) = A proof let Y be TopStruct ; ::_thesis: for A being Subset of Y holds the carrier of (Y | A) = A let A be Subset of Y; ::_thesis: the carrier of (Y | A) = A [#] (Y | A) = A by PRE_TOPC:def_5; hence the carrier of (Y | A) = A ; ::_thesis: verum end; theorem :: TEX_4:79 for Y being non empty TopStruct for A being non empty Subset of Y holds A is Subset of (Sspace A) proof let Y be non empty TopStruct ; ::_thesis: for A being non empty Subset of Y holds A is Subset of (Sspace A) let A be non empty Subset of Y; ::_thesis: A is Subset of (Sspace A) the carrier of (Sspace A) c= the carrier of (Sspace A) ; hence A is Subset of (Sspace A) by Lm3; ::_thesis: verum end; theorem :: TEX_4:80 for Y being non empty TopStruct for Y0 being SubSpace of Y for A being non empty Subset of Y st A is Subset of Y0 holds Sspace A is SubSpace of Y0 proof let Y be non empty TopStruct ; ::_thesis: for Y0 being SubSpace of Y for A being non empty Subset of Y st A is Subset of Y0 holds Sspace A is SubSpace of Y0 let Y0 be SubSpace of Y; ::_thesis: for A being non empty Subset of Y st A is Subset of Y0 holds Sspace A is SubSpace of Y0 let A be non empty Subset of Y; ::_thesis: ( A is Subset of Y0 implies Sspace A is SubSpace of Y0 ) assume A is Subset of Y0 ; ::_thesis: Sspace A is SubSpace of Y0 then A c= the carrier of Y0 ; then the carrier of (Sspace A) c= the carrier of Y0 by Lm3; hence Sspace A is SubSpace of Y0 by Lm2; ::_thesis: verum end; registration let Y be non trivial TopStruct ; cluster strict non proper for SubSpace of Y; existence ex b1 being SubSpace of Y st ( not b1 is proper & b1 is strict ) proof [#] Y = the carrier of Y ; then reconsider A0 = the carrier of Y as non empty Subset of Y ; set Y0 = Y | A0; take Y | A0 ; ::_thesis: ( not Y | A0 is proper & Y | A0 is strict ) A0 = [#] (Y | A0) by PRE_TOPC:def_5; hence ( not Y | A0 is proper & Y | A0 is strict ) by TEX_2:10; ::_thesis: verum end; end; registration let Y be non trivial TopStruct ; let A be non trivial Subset of Y; cluster Sspace A -> non trivial ; coherence not Sspace A is trivial by Lm3; end; registration let Y be non empty TopStruct ; let A be non proper Subset of Y; cluster Sspace A -> non proper ; coherence not Sspace A is proper proof now__::_thesis:_not_Sspace_A_is_proper assume A1: Sspace A is proper ; ::_thesis: contradiction the carrier of (Sspace A) = A by Lm3; hence contradiction by A1, TEX_2:8; ::_thesis: verum end; hence not Sspace A is proper ; ::_thesis: verum end; end; definition let Y be non empty TopStruct ; let A be Subset of Y; func MaxADSspace A -> strict SubSpace of Y means :Def18: :: TEX_4:def 18 the carrier of it = MaxADSet A; existence ex b1 being strict SubSpace of Y st the carrier of b1 = MaxADSet A proof set D = MaxADSet A; set Y0 = Y | (MaxADSet A); take Y | (MaxADSet A) ; ::_thesis: the carrier of (Y | (MaxADSet A)) = MaxADSet A MaxADSet A = [#] (Y | (MaxADSet A)) by PRE_TOPC:def_5; hence the carrier of (Y | (MaxADSet A)) = MaxADSet A ; ::_thesis: verum end; uniqueness for b1, b2 being strict SubSpace of Y st the carrier of b1 = MaxADSet A & the carrier of b2 = MaxADSet A holds b1 = b2 proof let Y1, Y2 be strict SubSpace of Y; ::_thesis: ( the carrier of Y1 = MaxADSet A & the carrier of Y2 = MaxADSet A implies Y1 = Y2 ) assume that A1: the carrier of Y1 = MaxADSet A and A2: the carrier of Y2 = MaxADSet A ; ::_thesis: Y1 = Y2 set A1 = the carrier of Y1; set A2 = the carrier of Y2; A3: the carrier of Y2 = [#] Y2 ; A4: the carrier of Y1 = [#] Y1 ; then the carrier of Y1 c= [#] Y by PRE_TOPC:def_4; then reconsider A1 = the carrier of Y1 as Subset of Y ; Y1 = Y | A1 by A4, PRE_TOPC:def_5; hence Y1 = Y2 by A1, A2, A3, PRE_TOPC:def_5; ::_thesis: verum end; end; :: deftheorem Def18 defines MaxADSspace TEX_4:def_18_:_ for Y being non empty TopStruct for A being Subset of Y for b3 being strict SubSpace of Y holds ( b3 = MaxADSspace A iff the carrier of b3 = MaxADSet A ); registration let Y be non empty TopStruct ; let A be non empty Subset of Y; cluster MaxADSspace A -> non empty strict ; coherence not MaxADSspace A is empty proof the carrier of (MaxADSspace A) = MaxADSet A by Def18; hence not the carrier of (MaxADSspace A) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum end; end; theorem :: TEX_4:81 for Y being non empty TopStruct for A being non empty Subset of Y holds A is Subset of (MaxADSspace A) proof let Y be non empty TopStruct ; ::_thesis: for A being non empty Subset of Y holds A is Subset of (MaxADSspace A) let A be non empty Subset of Y; ::_thesis: A is Subset of (MaxADSspace A) the carrier of (MaxADSspace A) = MaxADSet A by Def18; hence A is Subset of (MaxADSspace A) by Th32; ::_thesis: verum end; theorem :: TEX_4:82 for Y being non empty TopStruct for A being non empty Subset of Y holds Sspace A is SubSpace of MaxADSspace A proof let Y be non empty TopStruct ; ::_thesis: for A being non empty Subset of Y holds Sspace A is SubSpace of MaxADSspace A let A be non empty Subset of Y; ::_thesis: Sspace A is SubSpace of MaxADSspace A A1: the carrier of (Sspace A) = A by Lm3; the carrier of (MaxADSspace A) = MaxADSet A by Def18; hence Sspace A is SubSpace of MaxADSspace A by A1, Lm2, Th32; ::_thesis: verum end; theorem :: TEX_4:83 for Y being non empty TopStruct for x being Point of Y holds TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace {x}), the topology of (MaxADSspace {x}) #) proof let Y be non empty TopStruct ; ::_thesis: for x being Point of Y holds TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace {x}), the topology of (MaxADSspace {x}) #) let x be Point of Y; ::_thesis: TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace {x}), the topology of (MaxADSspace {x}) #) A1: the carrier of (MaxADSspace {x}) = MaxADSet {x} by Def18; the carrier of (MaxADSspace x) = MaxADSet x by Def17; hence TopStruct(# the carrier of (MaxADSspace x), the topology of (MaxADSspace x) #) = TopStruct(# the carrier of (MaxADSspace {x}), the topology of (MaxADSspace {x}) #) by A1, Th28, TSEP_1:5; ::_thesis: verum end; theorem :: TEX_4:84 for Y being non empty TopStruct for A, B being non empty Subset of Y st A c= B holds MaxADSspace A is SubSpace of MaxADSspace B proof let Y be non empty TopStruct ; ::_thesis: for A, B being non empty Subset of Y st A c= B holds MaxADSspace A is SubSpace of MaxADSspace B let A, B be non empty Subset of Y; ::_thesis: ( A c= B implies MaxADSspace A is SubSpace of MaxADSspace B ) assume A1: A c= B ; ::_thesis: MaxADSspace A is SubSpace of MaxADSspace B A2: the carrier of (MaxADSspace B) = MaxADSet B by Def18; the carrier of (MaxADSspace A) = MaxADSet A by Def18; hence MaxADSspace A is SubSpace of MaxADSspace B by A2, A1, Lm2, Th31; ::_thesis: verum end; theorem :: TEX_4:85 for Y being non empty TopStruct for A being non empty Subset of Y holds TopStruct(# the carrier of (MaxADSspace A), the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace (MaxADSet A)), the topology of (MaxADSspace (MaxADSet A)) #) proof let Y be non empty TopStruct ; ::_thesis: for A being non empty Subset of Y holds TopStruct(# the carrier of (MaxADSspace A), the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace (MaxADSet A)), the topology of (MaxADSspace (MaxADSet A)) #) let A be non empty Subset of Y; ::_thesis: TopStruct(# the carrier of (MaxADSspace A), the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace (MaxADSet A)), the topology of (MaxADSspace (MaxADSet A)) #) A1: the carrier of (MaxADSspace (MaxADSet A)) = MaxADSet (MaxADSet A) by Def18; the carrier of (MaxADSspace A) = MaxADSet A by Def18; hence TopStruct(# the carrier of (MaxADSspace A), the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace (MaxADSet A)), the topology of (MaxADSspace (MaxADSet A)) #) by A1, Th33, TSEP_1:5; ::_thesis: verum end; theorem :: TEX_4:86 for Y being non empty TopStruct for A, B being non empty Subset of Y st A is Subset of (MaxADSspace B) holds MaxADSspace A is SubSpace of MaxADSspace B proof let Y be non empty TopStruct ; ::_thesis: for A, B being non empty Subset of Y st A is Subset of (MaxADSspace B) holds MaxADSspace A is SubSpace of MaxADSspace B let A, B be non empty Subset of Y; ::_thesis: ( A is Subset of (MaxADSspace B) implies MaxADSspace A is SubSpace of MaxADSspace B ) assume A1: A is Subset of (MaxADSspace B) ; ::_thesis: MaxADSspace A is SubSpace of MaxADSspace B A2: the carrier of (MaxADSspace B) = MaxADSet B by Def18; the carrier of (MaxADSspace A) = MaxADSet A by Def18; hence MaxADSspace A is SubSpace of MaxADSspace B by A2, A1, Lm2, Th34; ::_thesis: verum end; theorem :: TEX_4:87 for Y being non empty TopStruct for A, B being non empty Subset of Y holds ( ( B is Subset of (MaxADSspace A) & A is Subset of (MaxADSspace B) ) iff TopStruct(# the carrier of (MaxADSspace A), the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace B), the topology of (MaxADSspace B) #) ) proof let Y be non empty TopStruct ; ::_thesis: for A, B being non empty Subset of Y holds ( ( B is Subset of (MaxADSspace A) & A is Subset of (MaxADSspace B) ) iff TopStruct(# the carrier of (MaxADSspace A), the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace B), the topology of (MaxADSspace B) #) ) let A, B be non empty Subset of Y; ::_thesis: ( ( B is Subset of (MaxADSspace A) & A is Subset of (MaxADSspace B) ) iff TopStruct(# the carrier of (MaxADSspace A), the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace B), the topology of (MaxADSspace B) #) ) A1: the carrier of (MaxADSspace B) = MaxADSet B by Def18; A2: the carrier of (MaxADSspace A) = MaxADSet A by Def18; hence ( B is Subset of (MaxADSspace A) & A is Subset of (MaxADSspace B) implies TopStruct(# the carrier of (MaxADSspace A), the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace B), the topology of (MaxADSspace B) #) ) by A1, Th35, TSEP_1:5; ::_thesis: ( TopStruct(# the carrier of (MaxADSspace A), the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace B), the topology of (MaxADSspace B) #) implies ( B is Subset of (MaxADSspace A) & A is Subset of (MaxADSspace B) ) ) assume TopStruct(# the carrier of (MaxADSspace A), the topology of (MaxADSspace A) #) = TopStruct(# the carrier of (MaxADSspace B), the topology of (MaxADSspace B) #) ; ::_thesis: ( B is Subset of (MaxADSspace A) & A is Subset of (MaxADSspace B) ) hence ( B is Subset of (MaxADSspace A) & A is Subset of (MaxADSspace B) ) by A2, A1, Th32; ::_thesis: verum end; registration let Y be non trivial TopStruct ; let A be non trivial Subset of Y; cluster MaxADSspace A -> non trivial strict ; coherence not MaxADSspace A is trivial proof not MaxADSet A is trivial ; hence not MaxADSspace A is trivial by Def18; ::_thesis: verum end; end; registration let Y be non empty TopStruct ; let A be non proper Subset of Y; cluster MaxADSspace A -> strict non proper ; coherence not MaxADSspace A is proper proof now__::_thesis:_not_MaxADSspace_A_is_proper assume A1: MaxADSspace A is proper ; ::_thesis: contradiction the carrier of (MaxADSspace A) = MaxADSet A by Def18; hence contradiction by A1, TEX_2:8; ::_thesis: verum end; hence not MaxADSspace A is proper ; ::_thesis: verum end; end; theorem :: TEX_4:88 for X being non empty TopSpace for X0 being open SubSpace of X for A being non empty Subset of X st A is Subset of X0 holds MaxADSspace A is SubSpace of X0 proof let X be non empty TopSpace; ::_thesis: for X0 being open SubSpace of X for A being non empty Subset of X st A is Subset of X0 holds MaxADSspace A is SubSpace of X0 let X0 be open SubSpace of X; ::_thesis: for A being non empty Subset of X st A is Subset of X0 holds MaxADSspace A is SubSpace of X0 let A be non empty Subset of X; ::_thesis: ( A is Subset of X0 implies MaxADSspace A is SubSpace of X0 ) reconsider D = the carrier of X0 as Subset of X by TSEP_1:1; A1: D is open by TSEP_1:16; assume A is Subset of X0 ; ::_thesis: MaxADSspace A is SubSpace of X0 then MaxADSet A c= D by A1, Th38; then the carrier of (MaxADSspace A) c= the carrier of X0 by Def18; hence MaxADSspace A is SubSpace of X0 by Lm2; ::_thesis: verum end; theorem :: TEX_4:89 for X being non empty TopSpace for X0 being closed SubSpace of X for A being non empty Subset of X st A is Subset of X0 holds MaxADSspace A is SubSpace of X0 proof let X be non empty TopSpace; ::_thesis: for X0 being closed SubSpace of X for A being non empty Subset of X st A is Subset of X0 holds MaxADSspace A is SubSpace of X0 let X0 be closed SubSpace of X; ::_thesis: for A being non empty Subset of X st A is Subset of X0 holds MaxADSspace A is SubSpace of X0 let A be non empty Subset of X; ::_thesis: ( A is Subset of X0 implies MaxADSspace A is SubSpace of X0 ) reconsider D = the carrier of X0 as Subset of X by TSEP_1:1; A1: D is closed by TSEP_1:11; assume A is Subset of X0 ; ::_thesis: MaxADSspace A is SubSpace of X0 then MaxADSet A c= D by A1, Th40; then the carrier of (MaxADSspace A) c= the carrier of X0 by Def18; hence MaxADSspace A is SubSpace of X0 by Lm2; ::_thesis: verum end;