:: TSP_2 semantic presentation begin definition let X be non empty TopSpace; let A be Subset of X; redefine attr A is T_0 means :Def1: :: TSP_2:def 1 for a, b being Point of X st a in A & b in A & a <> b holds MaxADSet a misses MaxADSet b; compatibility ( A is T_0 iff for a, b being Point of X st a in A & b in A & a <> b holds MaxADSet a misses MaxADSet b ) proof thus ( A is T_0 implies for a, b being Point of X st a in A & b in A & a <> b holds MaxADSet a misses MaxADSet b ) ::_thesis: ( ( for a, b being Point of X st a in A & b in A & a <> b holds MaxADSet a misses MaxADSet b ) implies A is T_0 ) proof assume A1: A is T_0 ; ::_thesis: for a, b being Point of X st a in A & b in A & a <> b holds MaxADSet a misses MaxADSet b let a, b be Point of X; ::_thesis: ( a in A & b in A & a <> b implies MaxADSet a misses MaxADSet b ) assume that A2: a in A and A3: b in A ; ::_thesis: ( not a <> b or MaxADSet a misses MaxADSet b ) assume A4: a <> b ; ::_thesis: MaxADSet a misses MaxADSet b now__::_thesis:_(_ex_V_being_Subset_of_X_st_ (_V_is_open_&_MaxADSet_a_c=_V_&_V_misses_MaxADSet_b_)_or_ex_W_being_Subset_of_X_st_ (_W_is_open_&_W_misses_MaxADSet_a_&_MaxADSet_b_c=_W_)_) percases ( ex V being Subset of X st ( V is open & a in V & not b in V ) or ex W being Subset of X st ( W is open & not a in W & b in W ) ) by A1, A2, A3, A4, TSP_1:def_8; suppose ex V being Subset of X st ( V is open & a in V & not b in V ) ; ::_thesis: ( ex V being Subset of X st ( V is open & MaxADSet a c= V & V misses MaxADSet b ) or ex W being Subset of X st ( W is open & W misses MaxADSet a & MaxADSet b c= W ) ) then consider V being Subset of X such that A5: V is open and A6: a in V and A7: not b in V ; now__::_thesis:_ex_V_being_Subset_of_X_st_ (_V_is_open_&_MaxADSet_a_c=_V_&_V_misses_MaxADSet_b_) take V = V; ::_thesis: ( V is open & MaxADSet a c= V & V misses MaxADSet b ) thus V is open by A5; ::_thesis: ( MaxADSet a c= V & V misses MaxADSet b ) thus MaxADSet a c= V by A5, A6, TEX_4:24; ::_thesis: V misses MaxADSet b b in ([#] X) \ V by A7, XBOOLE_0:def_5; then MaxADSet b c= V ` by A5, TEX_4:23; hence V misses MaxADSet b by SUBSET_1:23; ::_thesis: verum end; hence ( ex V being Subset of X st ( V is open & MaxADSet a c= V & V misses MaxADSet b ) or ex W being Subset of X st ( W is open & W misses MaxADSet a & MaxADSet b c= W ) ) ; ::_thesis: verum end; suppose ex W being Subset of X st ( W is open & not a in W & b in W ) ; ::_thesis: ( ex V being Subset of X st ( V is open & MaxADSet a c= V & V misses MaxADSet b ) or ex W being Subset of X st ( W is open & W misses MaxADSet a & MaxADSet b c= W ) ) then consider W being Subset of X such that A8: W is open and A9: not a in W and A10: b in W ; now__::_thesis:_ex_W_being_Subset_of_X_st_ (_W_is_open_&_W_misses_MaxADSet_a_&_MaxADSet_b_c=_W_) take W = W; ::_thesis: ( W is open & W misses MaxADSet a & MaxADSet b c= W ) thus W is open by A8; ::_thesis: ( W misses MaxADSet a & MaxADSet b c= W ) a in ([#] X) \ W by A9, XBOOLE_0:def_5; then MaxADSet a c= W ` by A8, TEX_4:23; hence W misses MaxADSet a by SUBSET_1:23; ::_thesis: MaxADSet b c= W thus MaxADSet b c= W by A8, A10, TEX_4:24; ::_thesis: verum end; hence ( ex V being Subset of X st ( V is open & MaxADSet a c= V & V misses MaxADSet b ) or ex W being Subset of X st ( W is open & W misses MaxADSet a & MaxADSet b c= W ) ) ; ::_thesis: verum end; end; end; hence MaxADSet a misses MaxADSet b by TEX_4:53; ::_thesis: verum end; assume A11: for a, b being Point of X st a in A & b in A & a <> b holds MaxADSet a misses MaxADSet b ; ::_thesis: A is T_0 now__::_thesis:_for_a,_b_being_Point_of_X_st_a_in_A_&_b_in_A_&_a_<>_b_&_(_for_V_being_Subset_of_X_holds_ (_not_V_is_open_or_not_a_in_V_or_b_in_V_)_)_holds_ ex_W_being_Subset_of_X_st_ (_W_is_open_&_not_a_in_W_&_b_in_W_) let a, b be Point of X; ::_thesis: ( a in A & b in A & a <> b & ( for V being Subset of X holds ( not V is open or not a in V or b in V ) ) implies ex W being Subset of X st ( W is open & not a in W & b in W ) ) assume that A12: a in A and A13: b in A ; ::_thesis: ( not a <> b or ex V being Subset of X st ( V is open & a in V & not b in V ) or ex W being Subset of X st ( W is open & not a in W & b in W ) ) assume a <> b ; ::_thesis: ( ex V being Subset of X st ( V is open & a in V & not b in V ) or ex W being Subset of X st ( W is open & not a in W & b in W ) ) then A14: MaxADSet a misses MaxADSet b by A11, A12, A13; now__::_thesis:_(_ex_V_being_Subset_of_X_st_ (_V_is_open_&_a_in_V_&_not_b_in_V_)_or_ex_W_being_Subset_of_X_st_ (_W_is_open_&_not_a_in_W_&_b_in_W_)_) percases ( ex V being Subset of X st ( V is open & MaxADSet a c= V & V misses MaxADSet b ) or ex W being Subset of X st ( W is open & W misses MaxADSet a & MaxADSet b c= W ) ) by A14, TEX_4:53; suppose ex V being Subset of X st ( V is open & MaxADSet a c= V & V misses MaxADSet b ) ; ::_thesis: ( ex V being Subset of X st ( V is open & a in V & not b in V ) or ex W being Subset of X st ( W is open & not a in W & b in W ) ) then consider V being Subset of X such that A15: V is open and A16: MaxADSet a c= V and A17: V misses MaxADSet b ; now__::_thesis:_ex_V_being_Subset_of_X_st_ (_V_is_open_&_a_in_V_&_not_b_in_V_) take V = V; ::_thesis: ( V is open & a in V & not b in V ) thus V is open by A15; ::_thesis: ( a in V & not b in V ) {a} c= MaxADSet a by TEX_4:18; then a in MaxADSet a by ZFMISC_1:31; hence a in V by A16; ::_thesis: not b in V now__::_thesis:_not_b_in_V {b} c= MaxADSet b by TEX_4:18; then A18: b in MaxADSet b by ZFMISC_1:31; assume b in V ; ::_thesis: contradiction hence contradiction by A17, A18, XBOOLE_0:3; ::_thesis: verum end; hence not b in V ; ::_thesis: verum end; hence ( ex V being Subset of X st ( V is open & a in V & not b in V ) or ex W being Subset of X st ( W is open & not a in W & b in W ) ) ; ::_thesis: verum end; suppose ex W being Subset of X st ( W is open & W misses MaxADSet a & MaxADSet b c= W ) ; ::_thesis: ( ex V being Subset of X st ( V is open & a in V & not b in V ) or ex W being Subset of X st ( W is open & not a in W & b in W ) ) then consider W being Subset of X such that A19: W is open and A20: W misses MaxADSet a and A21: MaxADSet b c= W ; now__::_thesis:_ex_W_being_Subset_of_X_st_ (_W_is_open_&_not_a_in_W_&_b_in_W_) take W = W; ::_thesis: ( W is open & not a in W & b in W ) thus W is open by A19; ::_thesis: ( not a in W & b in W ) now__::_thesis:_not_a_in_W {a} c= MaxADSet a by TEX_4:18; then A22: a in MaxADSet a by ZFMISC_1:31; assume a in W ; ::_thesis: contradiction hence contradiction by A20, A22, XBOOLE_0:3; ::_thesis: verum end; hence not a in W ; ::_thesis: b in W {b} c= MaxADSet b by TEX_4:18; then b in MaxADSet b by ZFMISC_1:31; hence b in W by A21; ::_thesis: verum end; hence ( ex V being Subset of X st ( V is open & a in V & not b in V ) or ex W being Subset of X st ( W is open & not a in W & b in W ) ) ; ::_thesis: verum end; end; end; hence ( ex V being Subset of X st ( V is open & a in V & not b in V ) or ex W being Subset of X st ( W is open & not a in W & b in W ) ) ; ::_thesis: verum end; hence A is T_0 by TSP_1:def_8; ::_thesis: verum end; end; :: deftheorem Def1 defines T_0 TSP_2:def_1_:_ for X being non empty TopSpace for A being Subset of X holds ( A is T_0 iff for a, b being Point of X st a in A & b in A & a <> b holds MaxADSet a misses MaxADSet b ); definition let X be non empty TopSpace; let A be Subset of X; redefine attr A is T_0 means :Def2: :: TSP_2:def 2 for a being Point of X st a in A holds A /\ (MaxADSet a) = {a}; compatibility ( A is T_0 iff for a being Point of X st a in A holds A /\ (MaxADSet a) = {a} ) proof thus ( A is T_0 implies for a being Point of X st a in A holds A /\ (MaxADSet a) = {a} ) ::_thesis: ( ( for a being Point of X st a in A holds A /\ (MaxADSet a) = {a} ) implies A is T_0 ) proof assume A1: A is T_0 ; ::_thesis: for a being Point of X st a in A holds A /\ (MaxADSet a) = {a} let a be Point of X; ::_thesis: ( a in A implies A /\ (MaxADSet a) = {a} ) assume A2: a in A ; ::_thesis: A /\ (MaxADSet a) = {a} assume A3: A /\ (MaxADSet a) <> {a} ; ::_thesis: contradiction {a} c= MaxADSet a by TEX_4:18; then a in MaxADSet a by ZFMISC_1:31; then a in A /\ (MaxADSet a) by A2, XBOOLE_0:def_4; then consider b being set such that A4: b in A /\ (MaxADSet a) and A5: b <> a by A3, ZFMISC_1:35; reconsider b = b as Point of X by A4; b in A by A4, XBOOLE_0:def_4; then A6: MaxADSet a misses MaxADSet b by A1, A2, A5, Def1; b in MaxADSet a by A4, XBOOLE_0:def_4; hence contradiction by A6, TEX_4:21; ::_thesis: verum end; assume A7: for a being Point of X st a in A holds A /\ (MaxADSet a) = {a} ; ::_thesis: A is T_0 now__::_thesis:_for_a,_b_being_Point_of_X_st_a_in_A_&_b_in_A_&_a_<>_b_holds_ not_MaxADSet_a_meets_MaxADSet_b let a, b be Point of X; ::_thesis: ( a in A & b in A & a <> b implies not MaxADSet a meets MaxADSet b ) assume that A8: a in A and A9: b in A ; ::_thesis: ( a <> b implies not MaxADSet a meets MaxADSet b ) A10: A /\ (MaxADSet a) = {a} by A7, A8; A11: A /\ (MaxADSet b) = {b} by A7, A9; assume A12: a <> b ; ::_thesis: not MaxADSet a meets MaxADSet b assume MaxADSet a meets MaxADSet b ; ::_thesis: contradiction then {a} = {b} by A10, A11, TEX_4:22; hence contradiction by A12, ZFMISC_1:3; ::_thesis: verum end; hence A is T_0 by Def1; ::_thesis: verum end; end; :: deftheorem Def2 defines T_0 TSP_2:def_2_:_ for X being non empty TopSpace for A being Subset of X holds ( A is T_0 iff for a being Point of X st a in A holds A /\ (MaxADSet a) = {a} ); definition let X be non empty TopSpace; let A be Subset of X; redefine attr A is T_0 means :: TSP_2:def 3 for a being Point of X st a in A holds ex D being Subset of X st ( D is maximal_anti-discrete & A /\ D = {a} ); compatibility ( A is T_0 iff for a being Point of X st a in A holds ex D being Subset of X st ( D is maximal_anti-discrete & A /\ D = {a} ) ) proof thus ( A is T_0 implies for a being Point of X st a in A holds ex D being Subset of X st ( D is maximal_anti-discrete & A /\ D = {a} ) ) ::_thesis: ( ( for a being Point of X st a in A holds ex D being Subset of X st ( D is maximal_anti-discrete & A /\ D = {a} ) ) implies A is T_0 ) proof assume A1: A is T_0 ; ::_thesis: for a being Point of X st a in A holds ex D being Subset of X st ( D is maximal_anti-discrete & A /\ D = {a} ) let a be Point of X; ::_thesis: ( a in A implies ex D being Subset of X st ( D is maximal_anti-discrete & A /\ D = {a} ) ) assume A2: a in A ; ::_thesis: ex D being Subset of X st ( D is maximal_anti-discrete & A /\ D = {a} ) take D = MaxADSet a; ::_thesis: ( D is maximal_anti-discrete & A /\ D = {a} ) thus D is maximal_anti-discrete by TEX_4:20; ::_thesis: A /\ D = {a} thus A /\ D = {a} by A1, A2, Def2; ::_thesis: verum end; assume A3: for a being Point of X st a in A holds ex D being Subset of X st ( D is maximal_anti-discrete & A /\ D = {a} ) ; ::_thesis: A is T_0 now__::_thesis:_for_a_being_Point_of_X_st_a_in_A_holds_ A_/\_(MaxADSet_a)_=_{a} let a be Point of X; ::_thesis: ( a in A implies A /\ (MaxADSet a) = {a} ) assume a in A ; ::_thesis: A /\ (MaxADSet a) = {a} then consider D being Subset of X such that A4: D is maximal_anti-discrete and A5: A /\ D = {a} by A3; a in A /\ D by A5, ZFMISC_1:31; then a in D by XBOOLE_0:def_4; hence A /\ (MaxADSet a) = {a} by A4, A5, TEX_4:27; ::_thesis: verum end; hence A is T_0 by Def2; ::_thesis: verum end; end; :: deftheorem defines T_0 TSP_2:def_3_:_ for X being non empty TopSpace for A being Subset of X holds ( A is T_0 iff for a being Point of X st a in A holds ex D being Subset of X st ( D is maximal_anti-discrete & A /\ D = {a} ) ); definition let Y be TopStruct ; let IT be Subset of Y; attrIT is maximal_T_0 means :Def4: :: TSP_2:def 4 ( IT is T_0 & ( for D being Subset of Y st D is T_0 & IT c= D holds IT = D ) ); end; :: deftheorem Def4 defines maximal_T_0 TSP_2:def_4_:_ for Y being TopStruct for IT being Subset of Y holds ( IT is maximal_T_0 iff ( IT is T_0 & ( for D being Subset of Y st D is T_0 & IT c= D holds IT = D ) ) ); theorem :: TSP_2:1 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_T_0 holds D1 is maximal_T_0 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_T_0 holds D1 is maximal_T_0 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_T_0 holds D1 is maximal_T_0 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_T_0 implies D1 is maximal_T_0 ) 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_T_0 or D1 is maximal_T_0 ) assume A2: D0 = D1 ; ::_thesis: ( not D0 is maximal_T_0 or D1 is maximal_T_0 ) assume A3: D0 is maximal_T_0 ; ::_thesis: D1 is maximal_T_0 A4: now__::_thesis:_for_D_being_Subset_of_Y1_st_D_is_T_0_&_D1_c=_D_holds_ D1_=_D let D be Subset of Y1; ::_thesis: ( D is T_0 & D1 c= D implies D1 = D ) reconsider E = D as Subset of Y0 by A1; assume D is T_0 ; ::_thesis: ( D1 c= D implies D1 = D ) then A5: E is T_0 by A1, TSP_1:3; assume D1 c= D ; ::_thesis: D1 = D hence D1 = D by A2, A3, A5, Def4; ::_thesis: verum end; D0 is T_0 by A3, Def4; then D1 is T_0 by A1, A2, TSP_1:3; hence D1 is maximal_T_0 by A4, Def4; ::_thesis: verum end; definition let X be non empty TopSpace; let M be Subset of X; redefine attr M is maximal_T_0 means :Def5: :: TSP_2:def 5 ( M is T_0 & MaxADSet M = the carrier of X ); compatibility ( M is maximal_T_0 iff ( M is T_0 & MaxADSet M = the carrier of X ) ) proof thus ( M is maximal_T_0 implies ( M is T_0 & MaxADSet M = the carrier of X ) ) ::_thesis: ( M is T_0 & MaxADSet M = the carrier of X implies M is maximal_T_0 ) proof assume A1: M is maximal_T_0 ; ::_thesis: ( M is T_0 & MaxADSet M = the carrier of X ) hence A2: M is T_0 by Def4; ::_thesis: MaxADSet M = the carrier of X the carrier of X c= MaxADSet M proof assume not the carrier of X c= MaxADSet M ; ::_thesis: contradiction then consider x being set such that A3: x in the carrier of X and A4: not x in MaxADSet M by TARSKI:def_3; reconsider x = x as Point of X by A3; set A = M \/ {x}; for a being Point of X st a in M \/ {x} holds (M \/ {x}) /\ (MaxADSet a) = {a} proof let a be Point of X; ::_thesis: ( a in M \/ {x} implies (M \/ {x}) /\ (MaxADSet a) = {a} ) assume a in M \/ {x} ; ::_thesis: (M \/ {x}) /\ (MaxADSet a) = {a} then A5: ( a in M or a in {x} ) by XBOOLE_0:def_3; now__::_thesis:_(M_\/_{x})_/\_(MaxADSet_a)_=_{a} percases ( a in M or a = x ) by A5, TARSKI:def_1; supposeA6: a in M ; ::_thesis: (M \/ {x}) /\ (MaxADSet a) = {a} {x} /\ (MaxADSet a) = {} proof assume {x} /\ (MaxADSet a) <> {} ; ::_thesis: contradiction then {x} meets MaxADSet a by XBOOLE_0:def_7; then A7: x in MaxADSet a by ZFMISC_1:50; {a} c= M by A6, ZFMISC_1:31; then MaxADSet {a} c= MaxADSet M by TEX_4:31; then MaxADSet a c= MaxADSet M by TEX_4:28; hence contradiction by A4, A7; ::_thesis: verum end; then (M \/ {x}) /\ (MaxADSet a) = (M /\ (MaxADSet a)) \/ {} by XBOOLE_1:23 .= M /\ (MaxADSet a) ; hence (M \/ {x}) /\ (MaxADSet a) = {a} by A2, A6, Def2; ::_thesis: verum end; supposeA8: a = x ; ::_thesis: (M \/ {x}) /\ (MaxADSet a) = {a} then A9: {x} c= MaxADSet a by TEX_4:18; M /\ (MaxADSet a) = {} proof A10: M c= MaxADSet M by TEX_4:32; assume M /\ (MaxADSet a) <> {} ; ::_thesis: contradiction then (MaxADSet a) /\ (MaxADSet M) <> {} by A10, XBOOLE_1:3, XBOOLE_1:26; then MaxADSet a meets MaxADSet M by XBOOLE_0:def_7; then A11: MaxADSet a c= MaxADSet M by TEX_4:30; x in MaxADSet a by A9, ZFMISC_1:31; hence contradiction by A4, A11; ::_thesis: verum end; then (M \/ {x}) /\ (MaxADSet a) = {} \/ ({x} /\ (MaxADSet a)) by XBOOLE_1:23 .= {x} /\ (MaxADSet a) ; hence (M \/ {x}) /\ (MaxADSet a) = {a} by A8, TEX_4:18, XBOOLE_1:28; ::_thesis: verum end; end; end; hence (M \/ {x}) /\ (MaxADSet a) = {a} ; ::_thesis: verum end; then A12: M \/ {x} is T_0 by Def2; A13: M c= MaxADSet M by TEX_4:32; A14: {x} c= M \/ {x} by XBOOLE_1:7; M c= M \/ {x} by XBOOLE_1:7; then M = M \/ {x} by A1, A12, Def4; then x in M by A14, ZFMISC_1:31; hence contradiction by A4, A13; ::_thesis: verum end; hence MaxADSet M = the carrier of X by XBOOLE_0:def_10; ::_thesis: verum end; assume A15: M is T_0 ; ::_thesis: ( not MaxADSet M = the carrier of X or M is maximal_T_0 ) assume A16: MaxADSet M = the carrier of X ; ::_thesis: M is maximal_T_0 for D being Subset of X st D is T_0 & M c= D holds M = D proof let D be Subset of X; ::_thesis: ( D is T_0 & M c= D implies M = D ) assume A17: D is T_0 ; ::_thesis: ( not M c= D or M = D ) assume A18: M c= D ; ::_thesis: M = D D c= M proof assume not D c= M ; ::_thesis: contradiction then consider x being set such that A19: x in D and A20: not x in M by TARSKI:def_3; A21: x in the carrier of X by A19; reconsider x = x as Point of X by A19; x in union { (MaxADSet a) where a is Point of X : a in M } by A16, A21, TEX_4:def_11; then consider C being set such that A22: x in C and A23: C in { (MaxADSet a) where a is Point of X : a in M } by TARSKI:def_4; consider a being Point of X such that A24: C = MaxADSet a and A25: a in M by A23; M /\ (MaxADSet x) c= D /\ (MaxADSet x) by A18, XBOOLE_1:26; then A26: M /\ (MaxADSet x) c= {x} by A17, A19, Def2; MaxADSet a = MaxADSet x by A22, A24, TEX_4:21; then M /\ (MaxADSet x) = {a} by A15, A25, Def2; hence contradiction by A20, A25, A26, ZFMISC_1:18; ::_thesis: verum end; hence M = D by A18, XBOOLE_0:def_10; ::_thesis: verum end; hence M is maximal_T_0 by A15, Def4; ::_thesis: verum end; end; :: deftheorem Def5 defines maximal_T_0 TSP_2:def_5_:_ for X being non empty TopSpace for M being Subset of X holds ( M is maximal_T_0 iff ( M is T_0 & MaxADSet M = the carrier of X ) ); theorem Th2: :: TSP_2:2 for X being non empty TopSpace for M being Subset of X st M is maximal_T_0 holds M is dense proof let X be non empty TopSpace; ::_thesis: for M being Subset of X st M is maximal_T_0 holds M is dense let M be Subset of X; ::_thesis: ( M is maximal_T_0 implies M is dense ) assume A1: M is maximal_T_0 ; ::_thesis: M is dense then MaxADSet M = [#] X by Def5; then A2: Cl (MaxADSet M) = MaxADSet M by PRE_TOPC:22; MaxADSet M = the carrier of X by A1, Def5; then Cl M = the carrier of X by A2, TEX_4:62; hence M is dense by TOPS_3:def_2; ::_thesis: verum end; theorem Th3: :: TSP_2:3 for X being non empty TopSpace for A being Subset of X st ( A is open or A is closed ) & A is maximal_T_0 holds not A is proper proof let X be non empty TopSpace; ::_thesis: for A being Subset of X st ( A is open or A is closed ) & A is maximal_T_0 holds not A is proper let A be Subset of X; ::_thesis: ( ( A is open or A is closed ) & A is maximal_T_0 implies not A is proper ) assume ( A is open or A is closed ) ; ::_thesis: ( not A is maximal_T_0 or not A is proper ) then A1: A = MaxADSet A by TEX_4:56, TEX_4:60; assume A is maximal_T_0 ; ::_thesis: not A is proper then A = the carrier of X by A1, Def5; hence not A is proper by SUBSET_1:def_6; ::_thesis: verum end; theorem Th4: :: TSP_2:4 for X being non empty TopSpace for A being empty Subset of X holds not A is maximal_T_0 proof let X be non empty TopSpace; ::_thesis: for A being empty Subset of X holds not A is maximal_T_0 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; let A be empty Subset of X; ::_thesis: not A is maximal_T_0 now__::_thesis:_ex_C_being_Element_of_bool_the_carrier_of_X_st_ (_C_is_T_0_&_A_c=_C_&_A_<>_C_) take C = {a}; ::_thesis: ( C is T_0 & A c= C & A <> C ) thus ( C is T_0 & A c= C & A <> C ) by TSP_1:12, XBOOLE_1:2; ::_thesis: verum end; hence not A is maximal_T_0 by Def4; ::_thesis: verum end; theorem Th5: :: TSP_2:5 for X being non empty TopSpace for M being Subset of X st M is maximal_T_0 holds for A being Subset of X st A is closed holds A = MaxADSet (M /\ A) proof let X be non empty TopSpace; ::_thesis: for M being Subset of X st M is maximal_T_0 holds for A being Subset of X st A is closed holds A = MaxADSet (M /\ A) let M be Subset of X; ::_thesis: ( M is maximal_T_0 implies for A being Subset of X st A is closed holds A = MaxADSet (M /\ A) ) assume A1: M is maximal_T_0 ; ::_thesis: for A being Subset of X st A is closed holds A = MaxADSet (M /\ A) let A be Subset of X; ::_thesis: ( A is closed implies A = MaxADSet (M /\ A) ) assume A2: A is closed ; ::_thesis: A = MaxADSet (M /\ A) then MaxADSet (M /\ A) = (MaxADSet M) /\ (MaxADSet A) by TEX_4:64; then A3: MaxADSet (M /\ A) = (MaxADSet M) /\ A by A2, TEX_4:60; A = the carrier of X /\ A by XBOOLE_1:28; hence A = MaxADSet (M /\ A) by A1, A3, Def5; ::_thesis: verum end; theorem Th6: :: TSP_2:6 for X being non empty TopSpace for M being Subset of X st M is maximal_T_0 holds for A being Subset of X st A is open holds A = MaxADSet (M /\ A) proof let X be non empty TopSpace; ::_thesis: for M being Subset of X st M is maximal_T_0 holds for A being Subset of X st A is open holds A = MaxADSet (M /\ A) let M be Subset of X; ::_thesis: ( M is maximal_T_0 implies for A being Subset of X st A is open holds A = MaxADSet (M /\ A) ) assume A1: M is maximal_T_0 ; ::_thesis: for A being Subset of X st A is open holds A = MaxADSet (M /\ A) let A be Subset of X; ::_thesis: ( A is open implies A = MaxADSet (M /\ A) ) assume A2: A is open ; ::_thesis: A = MaxADSet (M /\ A) then MaxADSet (M /\ A) = (MaxADSet M) /\ (MaxADSet A) by TEX_4:65; then A3: MaxADSet (M /\ A) = (MaxADSet M) /\ A by A2, TEX_4:56; A = the carrier of X /\ A by XBOOLE_1:28; hence A = MaxADSet (M /\ A) by A1, A3, Def5; ::_thesis: verum end; theorem :: TSP_2:7 for X being non empty TopSpace for M being Subset of X st M is maximal_T_0 holds for A being Subset of X holds Cl A = MaxADSet (M /\ (Cl A)) by Th5; theorem :: TSP_2:8 for X being non empty TopSpace for M being Subset of X st M is maximal_T_0 holds for A being Subset of X holds Int A = MaxADSet (M /\ (Int A)) by Th6; definition let X be non empty TopSpace; let M be Subset of X; redefine attr M is maximal_T_0 means :Def6: :: TSP_2:def 6 for x being Point of X ex a being Point of X st ( a in M & M /\ (MaxADSet x) = {a} ); compatibility ( M is maximal_T_0 iff for x being Point of X ex a being Point of X st ( a in M & M /\ (MaxADSet x) = {a} ) ) proof thus ( M is maximal_T_0 implies for x being Point of X ex a being Point of X st ( a in M & M /\ (MaxADSet x) = {a} ) ) ::_thesis: ( ( for x being Point of X ex a being Point of X st ( a in M & M /\ (MaxADSet x) = {a} ) ) implies M is maximal_T_0 ) proof assume A1: M is maximal_T_0 ; ::_thesis: for x being Point of X ex a being Point of X st ( a in M & M /\ (MaxADSet x) = {a} ) then A2: M is T_0 by Def4; let x be Point of X; ::_thesis: ex a being Point of X st ( a in M & M /\ (MaxADSet x) = {a} ) x in the carrier of X ; then x in MaxADSet M by A1, Def5; then x in union { (MaxADSet a) where a is Point of X : a in M } by TEX_4:def_11; then consider C being set such that A3: x in C and A4: C in { (MaxADSet a) where a is Point of X : a in M } by TARSKI:def_4; consider a being Point of X such that A5: C = MaxADSet a and A6: a in M by A4; MaxADSet a = MaxADSet x by A3, A5, TEX_4:21; then M /\ (MaxADSet x) = {a} by A2, A6, Def2; hence ex a being Point of X st ( a in M & M /\ (MaxADSet x) = {a} ) by A6; ::_thesis: verum end; assume A7: for x being Point of X ex a being Point of X st ( a in M & M /\ (MaxADSet x) = {a} ) ; ::_thesis: M is maximal_T_0 now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_X_holds_ x_in_MaxADSet_M let x be set ; ::_thesis: ( x in the carrier of X implies x in MaxADSet M ) A8: M c= MaxADSet M by TEX_4:32; assume x in the carrier of X ; ::_thesis: x in MaxADSet M then reconsider y = x as Point of X ; consider a being Point of X such that A9: a in M and A10: M /\ (MaxADSet y) = {a} by A7; {a} c= MaxADSet y by A10, XBOOLE_1:17; then a in MaxADSet y by ZFMISC_1:31; then (MaxADSet y) /\ (MaxADSet M) <> {} by A9, A8, XBOOLE_0:def_4; then MaxADSet y meets MaxADSet M by XBOOLE_0:def_7; then A11: MaxADSet y c= MaxADSet M by TEX_4:30; {y} c= MaxADSet y by TEX_4:18; then y in MaxADSet y by ZFMISC_1:31; hence x in MaxADSet M by A11; ::_thesis: verum end; then the carrier of X c= MaxADSet M by TARSKI:def_3; then A12: MaxADSet M = the carrier of X by XBOOLE_0:def_10; for b being Point of X st b in M holds M /\ (MaxADSet b) = {b} proof let b be Point of X; ::_thesis: ( b in M implies M /\ (MaxADSet b) = {b} ) A13: ex a being Point of X st ( a in M & M /\ (MaxADSet b) = {a} ) by A7; {b} c= MaxADSet b by TEX_4:18; then A14: b in MaxADSet b by ZFMISC_1:31; assume b in M ; ::_thesis: M /\ (MaxADSet b) = {b} then b in M /\ (MaxADSet b) by A14, XBOOLE_0:def_4; hence M /\ (MaxADSet b) = {b} by A13, TARSKI:def_1; ::_thesis: verum end; then M is T_0 by Def2; hence M is maximal_T_0 by A12, Def5; ::_thesis: verum end; end; :: deftheorem Def6 defines maximal_T_0 TSP_2:def_6_:_ for X being non empty TopSpace for M being Subset of X holds ( M is maximal_T_0 iff for x being Point of X ex a being Point of X st ( a in M & M /\ (MaxADSet x) = {a} ) ); theorem Th9: :: TSP_2:9 for X being non empty TopSpace for A being Subset of X st A is T_0 holds ex M being Subset of X st ( A c= M & M is maximal_T_0 ) proof let X be non empty TopSpace; ::_thesis: for A being Subset of X st A is T_0 holds ex M being Subset of X st ( A c= M & M is maximal_T_0 ) let A be Subset of X; ::_thesis: ( A is T_0 implies ex M being Subset of X st ( A c= M & M is maximal_T_0 ) ) set D = ([#] X) \ (MaxADSet A); set F = { (MaxADSet d) where d is Point of X : d in ([#] X) \ (MaxADSet A) } ; now__::_thesis:_for_C_being_set_st_C_in__{__(MaxADSet_d)_where_d_is_Point_of_X_:_d_in_([#]_X)_\_(MaxADSet_A)__}__holds_ C_in_bool_the_carrier_of_X let C be set ; ::_thesis: ( C in { (MaxADSet d) where d is Point of X : d in ([#] X) \ (MaxADSet A) } implies C in bool the carrier of X ) assume C in { (MaxADSet d) where d is Point of X : d in ([#] X) \ (MaxADSet A) } ; ::_thesis: C in bool the carrier of X then ex a being Point of X st ( C = MaxADSet a & a in ([#] X) \ (MaxADSet A) ) ; hence C in bool the carrier of X ; ::_thesis: verum end; then reconsider F = { (MaxADSet d) where d is Point of X : d in ([#] X) \ (MaxADSet A) } as Subset-Family of X by TARSKI:def_3; assume A1: A is T_0 ; ::_thesis: ex M being Subset of X st ( A c= M & M is maximal_T_0 ) defpred S1[ Subset of X, set ] means ( $2 in ([#] X) \ (MaxADSet A) & $2 in $1 ); A2: ([#] X) \ (MaxADSet A) = (MaxADSet A) ` ; then A3: MaxADSet A misses ([#] X) \ (MaxADSet A) by SUBSET_1:24; A c= MaxADSet A by TEX_4:32; then A misses ([#] X) \ (MaxADSet A) by A2, SUBSET_1:24; then A4: A /\ (([#] X) \ (MaxADSet A)) = {} by XBOOLE_0:def_7; reconsider F = F as Subset-Family of X ; A5: for S being Subset of X st S in F holds ex x being Point of X st S1[S,x] proof let S be Subset of X; ::_thesis: ( S in F implies ex x being Point of X st S1[S,x] ) assume S in F ; ::_thesis: ex x being Point of X st S1[S,x] then consider d being Point of X such that A6: S = MaxADSet d and A7: d in ([#] X) \ (MaxADSet A) ; take d ; ::_thesis: S1[S,d] {d} c= MaxADSet d by TEX_4:18; hence S1[S,d] by A6, A7, ZFMISC_1:31; ::_thesis: verum end; consider f being Function of F, the carrier of X such that A8: for S being Subset of X st S in F holds S1[S,f . S] from TEX_2:sch_1(A5); set M = A \/ (f .: F); now__::_thesis:_for_x_being_set_st_x_in_f_.:_F_holds_ x_in_([#]_X)_\_(MaxADSet_A) let x be set ; ::_thesis: ( x in f .: F implies x in ([#] X) \ (MaxADSet A) ) assume x in f .: F ; ::_thesis: x in ([#] X) \ (MaxADSet A) then ex S being set st ( S in F & S in F & x = f . S ) by FUNCT_2:64; hence x in ([#] X) \ (MaxADSet A) by A8; ::_thesis: verum end; then f .: F c= ([#] X) \ (MaxADSet A) by TARSKI:def_3; then A9: MaxADSet A misses f .: F by A3, XBOOLE_1:63; thus ex M being Subset of X st ( A c= M & M is maximal_T_0 ) ::_thesis: verum proof take A \/ (f .: F) ; ::_thesis: ( A c= A \/ (f .: F) & A \/ (f .: F) is maximal_T_0 ) thus A10: A c= A \/ (f .: F) by XBOOLE_1:7; ::_thesis: A \/ (f .: F) is maximal_T_0 for x being Point of X ex a being Point of X st ( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (MaxADSet x) = {a} ) proof let x be Point of X; ::_thesis: ex a being Point of X st ( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (MaxADSet x) = {a} ) A11: [#] X = (MaxADSet A) \/ (([#] X) \ (MaxADSet A)) by XBOOLE_1:45; now__::_thesis:_ex_a_being_Point_of_X_st_ (_a_in_A_\/_(f_.:_F)_&_(A_\/_(f_.:_F))_/\_(MaxADSet_x)_=_{a}_) percases ( x in MaxADSet A or x in ([#] X) \ (MaxADSet A) ) by A11, XBOOLE_0:def_3; supposeA12: x in MaxADSet A ; ::_thesis: ex a being Point of X st ( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (MaxADSet x) = {a} ) now__::_thesis:_ex_a_being_Point_of_X_st_ (_a_in_A_\/_(f_.:_F)_&_(A_\/_(f_.:_F))_/\_(MaxADSet_x)_=_{a}_) {x} c= MaxADSet A by A12, ZFMISC_1:31; then MaxADSet {x} c= MaxADSet A by TEX_4:34; then MaxADSet x c= MaxADSet A by TEX_4:28; then f .: F misses MaxADSet x by A9, XBOOLE_1:63; then (f .: F) /\ (MaxADSet x) = {} by XBOOLE_0:def_7; then A13: (A \/ (f .: F)) /\ (MaxADSet x) = (A /\ (MaxADSet x)) \/ {} by XBOOLE_1:23; x in union { (MaxADSet a) where a is Point of X : a in A } by A12, TEX_4:def_11; then consider C being set such that A14: x in C and A15: C in { (MaxADSet a) where a is Point of X : a in A } by TARSKI:def_4; consider a being Point of X such that A16: C = MaxADSet a and A17: a in A by A15; take a = a; ::_thesis: ( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (MaxADSet x) = {a} ) thus a in A \/ (f .: F) by A10, A17; ::_thesis: (A \/ (f .: F)) /\ (MaxADSet x) = {a} MaxADSet a = MaxADSet x by A14, A16, TEX_4:21; hence (A \/ (f .: F)) /\ (MaxADSet x) = {a} by A1, A17, A13, Def2; ::_thesis: verum end; hence ex a being Point of X st ( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (MaxADSet x) = {a} ) ; ::_thesis: verum end; supposeA18: x in ([#] X) \ (MaxADSet A) ; ::_thesis: ex a being Point of X st ( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (MaxADSet x) = {a} ) then A19: MaxADSet x in F ; now__::_thesis:_ex_a_being_Point_of_X_st_ (_a_in_A_\/_(f_.:_F)_&_(A_\/_(f_.:_F))_/\_(MaxADSet_x)_=_{a}_) reconsider a = f . (MaxADSet x) as Point of X by A19, FUNCT_2:5; take a = a; ::_thesis: ( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (MaxADSet x) = {a} ) A20: f .: F c= A \/ (f .: F) by XBOOLE_1:7; now__::_thesis:_for_y_being_set_st_y_in_(A_\/_(f_.:_F))_/\_(MaxADSet_x)_holds_ y_in_{a} let y be set ; ::_thesis: ( y in (A \/ (f .: F)) /\ (MaxADSet x) implies y in {a} ) assume A21: y in (A \/ (f .: F)) /\ (MaxADSet x) ; ::_thesis: y in {a} then reconsider z = y as Point of X ; A22: z in A \/ (f .: F) by A21, XBOOLE_0:def_4; A23: z in MaxADSet x by A21, XBOOLE_0:def_4; then A24: MaxADSet z = MaxADSet x by TEX_4:21; now__::_thesis:_MaxADSet_x_c=_([#]_X)_\_(MaxADSet_A) assume not MaxADSet x c= ([#] X) \ (MaxADSet A) ; ::_thesis: contradiction then MaxADSet x meets MaxADSet A by A2, SUBSET_1:23; then A25: MaxADSet x c= MaxADSet A by TEX_4:30; {x} c= MaxADSet x by TEX_4:18; then x in MaxADSet x by ZFMISC_1:31; hence contradiction by A3, A18, A25, XBOOLE_0:3; ::_thesis: verum end; then not z in A by A4, A23, XBOOLE_0:def_4; then z in f .: F by A22, XBOOLE_0:def_3; then consider C being set such that A26: C in F and C in F and A27: z = f . C by FUNCT_2:64; reconsider C = C as Subset of X by A26; consider w being Point of X such that A28: C = MaxADSet w and w in ([#] X) \ (MaxADSet A) by A26; z in MaxADSet w by A8, A26, A27, A28; then f . (MaxADSet w) = a by A24, TEX_4:21; hence y in {a} by A27, A28, TARSKI:def_1; ::_thesis: verum end; then A29: (A \/ (f .: F)) /\ (MaxADSet x) c= {a} by TARSKI:def_3; A30: a in f .: F by A19, FUNCT_2:35; hence a in A \/ (f .: F) by A20; ::_thesis: (A \/ (f .: F)) /\ (MaxADSet x) = {a} a in MaxADSet x by A8, A19; then A31: {a} c= MaxADSet x by ZFMISC_1:31; {a} c= A \/ (f .: F) by A20, A30, ZFMISC_1:31; then {a} c= (A \/ (f .: F)) /\ (MaxADSet x) by A31, XBOOLE_1:19; hence (A \/ (f .: F)) /\ (MaxADSet x) = {a} by A29, XBOOLE_0:def_10; ::_thesis: verum end; hence ex a being Point of X st ( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (MaxADSet x) = {a} ) ; ::_thesis: verum end; end; end; hence ex a being Point of X st ( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (MaxADSet x) = {a} ) ; ::_thesis: verum end; hence A \/ (f .: F) is maximal_T_0 by Def6; ::_thesis: verum end; end; theorem Th10: :: TSP_2:10 for X being non empty TopSpace ex M being Subset of X st M is maximal_T_0 proof let X be non empty TopSpace; ::_thesis: ex M being Subset of X st M is maximal_T_0 set A = {} X; {} X is discrete by TEX_2:29; then consider M being Subset of X such that {} X c= M and A1: M is maximal_T_0 by Th9, TSP_1:9; take M ; ::_thesis: M is maximal_T_0 thus M is maximal_T_0 by A1; ::_thesis: verum end; begin definition let Y be non empty TopStruct ; let IT be SubSpace of Y; attrIT is maximal_T_0 means :Def7: :: TSP_2:def 7 for A being Subset of Y st A = the carrier of IT holds A is maximal_T_0 ; end; :: deftheorem Def7 defines maximal_T_0 TSP_2:def_7_:_ for Y being non empty TopStruct for IT being SubSpace of Y holds ( IT is maximal_T_0 iff for A being Subset of Y st A = the carrier of IT holds A is maximal_T_0 ); theorem Th11: :: TSP_2:11 for Y being non empty TopStruct for Y0 being SubSpace of Y for A being Subset of Y st A = the carrier of Y0 holds ( A is maximal_T_0 iff Y0 is maximal_T_0 ) 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 holds ( A is maximal_T_0 iff Y0 is maximal_T_0 ) let Y0 be SubSpace of Y; ::_thesis: for A being Subset of Y st A = the carrier of Y0 holds ( A is maximal_T_0 iff Y0 is maximal_T_0 ) let A be Subset of Y; ::_thesis: ( A = the carrier of Y0 implies ( A is maximal_T_0 iff Y0 is maximal_T_0 ) ) assume A1: A = the carrier of Y0 ; ::_thesis: ( A is maximal_T_0 iff Y0 is maximal_T_0 ) hereby ::_thesis: ( Y0 is maximal_T_0 implies A is maximal_T_0 ) assume A is maximal_T_0 ; ::_thesis: Y0 is maximal_T_0 then for A being Subset of Y st A = the carrier of Y0 holds A is maximal_T_0 by A1; hence Y0 is maximal_T_0 by Def7; ::_thesis: verum end; thus ( Y0 is maximal_T_0 implies A is maximal_T_0 ) by A1, Def7; ::_thesis: verum end; Lm1: now__::_thesis:_for_Z_being_non_empty_TopStruct_ for_Z0_being_SubSpace_of_Z_holds_the_carrier_of_Z0_is_Subset_of_Z let Z be non empty TopStruct ; ::_thesis: for Z0 being SubSpace of Z holds the carrier of Z0 is Subset of Z let Z0 be SubSpace of Z; ::_thesis: the carrier of Z0 is Subset of Z [#] Z0 c= [#] Z by PRE_TOPC:def_4; hence the carrier of Z0 is Subset of Z ; ::_thesis: verum end; registration let Y be non empty TopStruct ; cluster non empty maximal_T_0 -> non empty V56() for SubSpace of Y; coherence for b1 being non empty SubSpace of Y st b1 is maximal_T_0 holds b1 is V56() proof let Y0 be non empty SubSpace of Y; ::_thesis: ( Y0 is maximal_T_0 implies Y0 is V56() ) reconsider A = the carrier of Y0 as Subset of Y by Lm1; assume Y0 is maximal_T_0 ; ::_thesis: Y0 is V56() then A is maximal_T_0 by Th11; then A is T_0 by Def4; hence Y0 is V56() by TSP_1:13; ::_thesis: verum end; cluster non empty V56() -> non empty non maximal_T_0 for SubSpace of Y; coherence for b1 being non empty SubSpace of Y st b1 is V56() holds not b1 is maximal_T_0 ; end; definition let X be non empty TopSpace; let X0 be non empty SubSpace of X; redefine attr X0 is maximal_T_0 means :: TSP_2:def 8 ( X0 is V56() & ( for Y0 being non empty V56() SubSpace of X st X0 is SubSpace of Y0 holds TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) ); compatibility ( X0 is maximal_T_0 iff ( X0 is V56() & ( for Y0 being non empty V56() SubSpace of X st X0 is SubSpace of Y0 holds TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) ) ) proof reconsider A = the carrier of X0 as Subset of X by TSEP_1:1; thus ( X0 is maximal_T_0 implies ( X0 is V56() & ( for Y0 being non empty V56() SubSpace of X st X0 is SubSpace of Y0 holds TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) ) ) ::_thesis: ( X0 is V56() & ( for Y0 being non empty V56() SubSpace of X st X0 is SubSpace of Y0 holds TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) implies X0 is maximal_T_0 ) proof assume X0 is maximal_T_0 ; ::_thesis: ( X0 is V56() & ( for Y0 being non empty V56() SubSpace of X st X0 is SubSpace of Y0 holds TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) ) then A1: A is maximal_T_0 by Th11; then A is T_0 by Def4; hence X0 is V56() by TSP_1:13; ::_thesis: for Y0 being non empty V56() SubSpace of X st X0 is SubSpace of Y0 holds TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) thus for Y0 being non empty V56() SubSpace of X st X0 is SubSpace of Y0 holds TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ::_thesis: verum proof let Y0 be non empty V56() SubSpace of X; ::_thesis: ( X0 is SubSpace of Y0 implies TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) reconsider D = the carrier of Y0 as Subset of X by TSEP_1:1; assume X0 is SubSpace of Y0 ; ::_thesis: TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) then A2: A c= D by TSEP_1:4; D is T_0 by TSP_1:13; then A = D by A1, A2, Def4; hence TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) by TSEP_1:5; ::_thesis: verum end; end; assume X0 is V56() ; ::_thesis: ( ex Y0 being non empty V56() SubSpace of X st ( X0 is SubSpace of Y0 & not TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) or X0 is maximal_T_0 ) then A3: A is T_0 by TSP_1:13; assume A4: for Y0 being non empty V56() SubSpace of X st X0 is SubSpace of Y0 holds TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ; ::_thesis: X0 is maximal_T_0 now__::_thesis:_for_D_being_Subset_of_X_st_D_is_T_0_&_A_c=_D_holds_ A_=_D let D be Subset of X; ::_thesis: ( D is T_0 & A c= D implies A = D ) assume A5: D is T_0 ; ::_thesis: ( A c= D implies A = D ) assume A6: A c= D ; ::_thesis: A = D then D <> {} ; then consider Y0 being non empty strict V56() SubSpace of X such that A7: D = the carrier of Y0 by A5, TSP_1:18; X0 is SubSpace of Y0 by A6, A7, TSEP_1:4; hence A = D by A4, A7; ::_thesis: verum end; then A is maximal_T_0 by A3, Def4; hence X0 is maximal_T_0 by Th11; ::_thesis: verum end; end; :: deftheorem defines maximal_T_0 TSP_2:def_8_:_ for X being non empty TopSpace for X0 being non empty SubSpace of X holds ( X0 is maximal_T_0 iff ( X0 is V56() & ( for Y0 being non empty V56() SubSpace of X st X0 is SubSpace of Y0 holds TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) ) ); theorem Th12: :: TSP_2:12 for X being non empty TopSpace for A0 being non empty Subset of X st A0 is maximal_T_0 holds ex X0 being non empty strict SubSpace of X st ( X0 is maximal_T_0 & A0 = the carrier of X0 ) proof let X be non empty TopSpace; ::_thesis: for A0 being non empty Subset of X st A0 is maximal_T_0 holds ex X0 being non empty strict SubSpace of X st ( X0 is maximal_T_0 & A0 = the carrier of X0 ) let A0 be non empty Subset of X; ::_thesis: ( A0 is maximal_T_0 implies ex X0 being non empty strict SubSpace of X st ( X0 is maximal_T_0 & A0 = the carrier of X0 ) ) assume A1: A0 is maximal_T_0 ; ::_thesis: ex X0 being non empty strict SubSpace of X st ( X0 is maximal_T_0 & A0 = the carrier of X0 ) consider X0 being non empty strict SubSpace of X such that A2: A0 = the carrier of X0 by TSEP_1:10; take X0 ; ::_thesis: ( X0 is maximal_T_0 & A0 = the carrier of X0 ) thus ( X0 is maximal_T_0 & A0 = the carrier of X0 ) by A1, A2, Th11; ::_thesis: verum end; registration let X be non empty TopSpace; cluster maximal_T_0 -> dense for SubSpace of X; coherence for b1 being SubSpace of X st b1 is maximal_T_0 holds b1 is dense proof let X0 be SubSpace of X; ::_thesis: ( X0 is maximal_T_0 implies X0 is dense ) reconsider A = the carrier of X0 as Subset of X by Lm1; assume X0 is maximal_T_0 ; ::_thesis: X0 is dense then A is maximal_T_0 by Th11; then A is dense by Th2; hence X0 is dense by TEX_3:9; ::_thesis: verum end; cluster non dense -> non maximal_T_0 for SubSpace of X; coherence for b1 being SubSpace of X st not b1 is dense holds not b1 is maximal_T_0 ; cluster open maximal_T_0 -> non proper for SubSpace of X; coherence for b1 being SubSpace of X st b1 is open & b1 is maximal_T_0 holds not b1 is proper proof let X0 be SubSpace of X; ::_thesis: ( X0 is open & X0 is maximal_T_0 implies not X0 is proper ) reconsider A = the carrier of X0 as Subset of X by Lm1; assume X0 is open ; ::_thesis: ( not X0 is maximal_T_0 or not X0 is proper ) then A1: A is open by TSEP_1:16; assume X0 is maximal_T_0 ; ::_thesis: not X0 is proper then A is maximal_T_0 by Th11; then not A is proper by A1, Th3; hence not X0 is proper by TEX_2:8; ::_thesis: verum end; cluster open proper -> non maximal_T_0 for SubSpace of X; coherence for b1 being SubSpace of X st b1 is open & b1 is proper holds not b1 is maximal_T_0 ; cluster proper maximal_T_0 -> non open for SubSpace of X; coherence for b1 being SubSpace of X st b1 is proper & b1 is maximal_T_0 holds not b1 is open ; cluster closed maximal_T_0 -> non proper for SubSpace of X; coherence for b1 being SubSpace of X st b1 is closed & b1 is maximal_T_0 holds not b1 is proper proof let X0 be SubSpace of X; ::_thesis: ( X0 is closed & X0 is maximal_T_0 implies not X0 is proper ) reconsider A = the carrier of X0 as Subset of X by Lm1; assume X0 is closed ; ::_thesis: ( not X0 is maximal_T_0 or not X0 is proper ) then A2: A is closed by TSEP_1:11; assume X0 is maximal_T_0 ; ::_thesis: not X0 is proper then A is maximal_T_0 by Th11; then not A is proper by A2, Th3; hence not X0 is proper by TEX_2:8; ::_thesis: verum end; cluster closed proper -> non maximal_T_0 for SubSpace of X; coherence for b1 being SubSpace of X st b1 is closed & b1 is proper holds not b1 is maximal_T_0 ; cluster proper maximal_T_0 -> non closed for SubSpace of X; coherence for b1 being SubSpace of X st b1 is proper & b1 is maximal_T_0 holds not b1 is closed ; end; theorem :: TSP_2:13 for X being non empty TopSpace for Y0 being non empty V56() SubSpace of X ex X0 being strict SubSpace of X st ( Y0 is SubSpace of X0 & X0 is maximal_T_0 ) proof let X be non empty TopSpace; ::_thesis: for Y0 being non empty V56() SubSpace of X ex X0 being strict SubSpace of X st ( Y0 is SubSpace of X0 & X0 is maximal_T_0 ) let Y0 be non empty V56() SubSpace of X; ::_thesis: ex X0 being strict SubSpace of X st ( Y0 is SubSpace of X0 & X0 is maximal_T_0 ) reconsider A = the carrier of Y0 as Subset of X by Lm1; A is T_0 by TSP_1:13; then consider M being Subset of X such that A1: A c= M and A2: M is maximal_T_0 by Th9; not M is empty by A2, Th4; then consider X0 being non empty strict SubSpace of X such that A3: X0 is maximal_T_0 and A4: M = the carrier of X0 by A2, Th12; take X0 ; ::_thesis: ( Y0 is SubSpace of X0 & X0 is maximal_T_0 ) thus ( Y0 is SubSpace of X0 & X0 is maximal_T_0 ) by A1, A3, A4, TSEP_1:4; ::_thesis: verum end; registration let X be non empty TopSpace; cluster non empty strict TopSpace-like maximal_T_0 for SubSpace of X; existence ex b1 being SubSpace of X st ( b1 is maximal_T_0 & b1 is strict & not b1 is empty ) proof consider M being Subset of X such that A1: M is maximal_T_0 by Th10; not M is empty by A1, Th4; then consider X0 being non empty strict SubSpace of X such that A2: X0 is maximal_T_0 and M = the carrier of X0 by A1, Th12; take X0 ; ::_thesis: ( X0 is maximal_T_0 & X0 is strict & not X0 is empty ) thus ( X0 is maximal_T_0 & X0 is strict & not X0 is empty ) by A2; ::_thesis: verum end; end; definition let X be non empty TopSpace; mode maximal_Kolmogorov_subspace of X is maximal_T_0 SubSpace of X; end; theorem Th14: :: TSP_2:14 for X being non empty TopSpace for X0 being maximal_Kolmogorov_subspace of X for G being Subset of X for G0 being Subset of X0 st G0 = G holds ( G0 is open iff ( MaxADSet G is open & G0 = (MaxADSet G) /\ the carrier of X0 ) ) proof let X be non empty TopSpace; ::_thesis: for X0 being maximal_Kolmogorov_subspace of X for G being Subset of X for G0 being Subset of X0 st G0 = G holds ( G0 is open iff ( MaxADSet G is open & G0 = (MaxADSet G) /\ the carrier of X0 ) ) let X0 be maximal_Kolmogorov_subspace of X; ::_thesis: for G being Subset of X for G0 being Subset of X0 st G0 = G holds ( G0 is open iff ( MaxADSet G is open & G0 = (MaxADSet G) /\ the carrier of X0 ) ) let G be Subset of X; ::_thesis: for G0 being Subset of X0 st G0 = G holds ( G0 is open iff ( MaxADSet G is open & G0 = (MaxADSet G) /\ the carrier of X0 ) ) let G0 be Subset of X0; ::_thesis: ( G0 = G implies ( G0 is open iff ( MaxADSet G is open & G0 = (MaxADSet G) /\ the carrier of X0 ) ) ) reconsider M = the carrier of X0 as Subset of X by Lm1; assume A1: G0 = G ; ::_thesis: ( G0 is open iff ( MaxADSet G is open & G0 = (MaxADSet G) /\ the carrier of X0 ) ) A2: M is maximal_T_0 by Th11; thus ( G0 is open implies ( MaxADSet G is open & G0 = (MaxADSet G) /\ the carrier of X0 ) ) ::_thesis: ( MaxADSet G is open & G0 = (MaxADSet G) /\ the carrier of X0 implies G0 is open ) proof assume G0 is open ; ::_thesis: ( MaxADSet G is open & G0 = (MaxADSet G) /\ the carrier of X0 ) then A3: ex H being Subset of X st ( H is open & G0 = H /\ M ) by TSP_1:def_1; hence MaxADSet G is open by A2, A1, Th6; ::_thesis: G0 = (MaxADSet G) /\ the carrier of X0 thus G0 = (MaxADSet G) /\ the carrier of X0 by A2, A1, A3, Th6; ::_thesis: verum end; assume A4: MaxADSet G is open ; ::_thesis: ( not G0 = (MaxADSet G) /\ the carrier of X0 or G0 is open ) assume G0 = (MaxADSet G) /\ the carrier of X0 ; ::_thesis: G0 is open hence G0 is open by A4, TSP_1:def_1; ::_thesis: verum end; theorem :: TSP_2:15 for X being non empty TopSpace for X0 being maximal_Kolmogorov_subspace of X for G being Subset of X holds ( G is open iff ( G = MaxADSet G & ex G0 being Subset of X0 st ( G0 is open & G0 = G /\ the carrier of X0 ) ) ) proof let X be non empty TopSpace; ::_thesis: for X0 being maximal_Kolmogorov_subspace of X for G being Subset of X holds ( G is open iff ( G = MaxADSet G & ex G0 being Subset of X0 st ( G0 is open & G0 = G /\ the carrier of X0 ) ) ) let X0 be maximal_Kolmogorov_subspace of X; ::_thesis: for G being Subset of X holds ( G is open iff ( G = MaxADSet G & ex G0 being Subset of X0 st ( G0 is open & G0 = G /\ the carrier of X0 ) ) ) let G be Subset of X; ::_thesis: ( G is open iff ( G = MaxADSet G & ex G0 being Subset of X0 st ( G0 is open & G0 = G /\ the carrier of X0 ) ) ) reconsider M = the carrier of X0 as Subset of X by Lm1; thus ( G is open implies ( G = MaxADSet G & ex G0 being Subset of X0 st ( G0 is open & G0 = G /\ the carrier of X0 ) ) ) ::_thesis: ( G = MaxADSet G & ex G0 being Subset of X0 st ( G0 is open & G0 = G /\ the carrier of X0 ) implies G is open ) proof reconsider G0 = G /\ M as Subset of X0 by XBOOLE_1:17; reconsider G0 = G0 as Subset of X0 ; assume A1: G is open ; ::_thesis: ( G = MaxADSet G & ex G0 being Subset of X0 st ( G0 is open & G0 = G /\ the carrier of X0 ) ) hence G = MaxADSet G by TEX_4:56; ::_thesis: ex G0 being Subset of X0 st ( G0 is open & G0 = G /\ the carrier of X0 ) take G0 ; ::_thesis: ( G0 is open & G0 = G /\ the carrier of X0 ) thus G0 is open by A1, TSP_1:def_1; ::_thesis: G0 = G /\ the carrier of X0 thus G0 = G /\ the carrier of X0 ; ::_thesis: verum end; assume A2: G = MaxADSet G ; ::_thesis: ( for G0 being Subset of X0 holds ( not G0 is open or not G0 = G /\ the carrier of X0 ) or G is open ) given G0 being Subset of X0 such that A3: G0 is open and A4: G0 = G /\ the carrier of X0 ; ::_thesis: G is open set E = G0; G0 c= M ; then reconsider E = G0 as Subset of X by XBOOLE_1:1; A5: E c= MaxADSet G by A2, A4, XBOOLE_1:17; A6: M is maximal_T_0 by Th11; for x being set st x in G holds x in MaxADSet E proof let x be set ; ::_thesis: ( x in G implies x in MaxADSet E ) assume A7: x in G ; ::_thesis: x in MaxADSet E then reconsider a = x as Point of X ; consider b being Point of X such that A8: b in M and A9: M /\ (MaxADSet a) = {b} by A6, Def6; A10: {b} c= MaxADSet a by A9, XBOOLE_1:17; {a} c= G by A7, ZFMISC_1:31; then MaxADSet {a} c= G by A2, TEX_4:34; then MaxADSet a c= G by TEX_4:28; then {b} c= G by A10, XBOOLE_1:1; then b in G by ZFMISC_1:31; then b in E by A4, A8, XBOOLE_0:def_4; then {b} c= E by ZFMISC_1:31; then MaxADSet {b} c= MaxADSet E by TEX_4:31; then A11: MaxADSet b c= MaxADSet E by TEX_4:28; b in MaxADSet a by A10, ZFMISC_1:31; then MaxADSet b = MaxADSet a by TEX_4:21; then {a} c= MaxADSet b by TEX_4:18; then a in MaxADSet b by ZFMISC_1:31; hence x in MaxADSet E by A11; ::_thesis: verum end; then A12: G c= MaxADSet E by TARSKI:def_3; MaxADSet E is open by A3, Th14; hence G is open by A2, A5, A12, TEX_4:35; ::_thesis: verum end; theorem Th16: :: TSP_2:16 for X being non empty TopSpace for X0 being maximal_Kolmogorov_subspace of X for F being Subset of X for F0 being Subset of X0 st F0 = F holds ( F0 is closed iff ( MaxADSet F is closed & F0 = (MaxADSet F) /\ the carrier of X0 ) ) proof let X be non empty TopSpace; ::_thesis: for X0 being maximal_Kolmogorov_subspace of X for F being Subset of X for F0 being Subset of X0 st F0 = F holds ( F0 is closed iff ( MaxADSet F is closed & F0 = (MaxADSet F) /\ the carrier of X0 ) ) let X0 be maximal_Kolmogorov_subspace of X; ::_thesis: for F being Subset of X for F0 being Subset of X0 st F0 = F holds ( F0 is closed iff ( MaxADSet F is closed & F0 = (MaxADSet F) /\ the carrier of X0 ) ) reconsider M = the carrier of X0 as Subset of X by TSEP_1:1; let F be Subset of X; ::_thesis: for F0 being Subset of X0 st F0 = F holds ( F0 is closed iff ( MaxADSet F is closed & F0 = (MaxADSet F) /\ the carrier of X0 ) ) let F0 be Subset of X0; ::_thesis: ( F0 = F implies ( F0 is closed iff ( MaxADSet F is closed & F0 = (MaxADSet F) /\ the carrier of X0 ) ) ) assume A1: F0 = F ; ::_thesis: ( F0 is closed iff ( MaxADSet F is closed & F0 = (MaxADSet F) /\ the carrier of X0 ) ) A2: M is maximal_T_0 by Th11; thus ( F0 is closed implies ( MaxADSet F is closed & F0 = (MaxADSet F) /\ the carrier of X0 ) ) ::_thesis: ( MaxADSet F is closed & F0 = (MaxADSet F) /\ the carrier of X0 implies F0 is closed ) proof assume F0 is closed ; ::_thesis: ( MaxADSet F is closed & F0 = (MaxADSet F) /\ the carrier of X0 ) then A3: ex H being Subset of X st ( H is closed & F0 = H /\ M ) by TSP_1:def_2; hence MaxADSet F is closed by A2, A1, Th5; ::_thesis: F0 = (MaxADSet F) /\ the carrier of X0 thus F0 = (MaxADSet F) /\ the carrier of X0 by A2, A1, A3, Th5; ::_thesis: verum end; assume A4: MaxADSet F is closed ; ::_thesis: ( not F0 = (MaxADSet F) /\ the carrier of X0 or F0 is closed ) assume F0 = (MaxADSet F) /\ the carrier of X0 ; ::_thesis: F0 is closed hence F0 is closed by A4, TSP_1:def_2; ::_thesis: verum end; theorem :: TSP_2:17 for X being non empty TopSpace for X0 being maximal_Kolmogorov_subspace of X for F being Subset of X holds ( F is closed iff ( F = MaxADSet F & ex F0 being Subset of X0 st ( F0 is closed & F0 = F /\ the carrier of X0 ) ) ) proof let X be non empty TopSpace; ::_thesis: for X0 being maximal_Kolmogorov_subspace of X for F being Subset of X holds ( F is closed iff ( F = MaxADSet F & ex F0 being Subset of X0 st ( F0 is closed & F0 = F /\ the carrier of X0 ) ) ) let X0 be maximal_Kolmogorov_subspace of X; ::_thesis: for F being Subset of X holds ( F is closed iff ( F = MaxADSet F & ex F0 being Subset of X0 st ( F0 is closed & F0 = F /\ the carrier of X0 ) ) ) reconsider M = the carrier of X0 as Subset of X by TSEP_1:1; let F be Subset of X; ::_thesis: ( F is closed iff ( F = MaxADSet F & ex F0 being Subset of X0 st ( F0 is closed & F0 = F /\ the carrier of X0 ) ) ) thus ( F is closed implies ( F = MaxADSet F & ex F0 being Subset of X0 st ( F0 is closed & F0 = F /\ the carrier of X0 ) ) ) ::_thesis: ( F = MaxADSet F & ex F0 being Subset of X0 st ( F0 is closed & F0 = F /\ the carrier of X0 ) implies F is closed ) proof set F0 = F /\ M; reconsider F0 = F /\ M as Subset of X0 by XBOOLE_1:17; assume A1: F is closed ; ::_thesis: ( F = MaxADSet F & ex F0 being Subset of X0 st ( F0 is closed & F0 = F /\ the carrier of X0 ) ) hence F = MaxADSet F by TEX_4:60; ::_thesis: ex F0 being Subset of X0 st ( F0 is closed & F0 = F /\ the carrier of X0 ) take F0 ; ::_thesis: ( F0 is closed & F0 = F /\ the carrier of X0 ) thus F0 is closed by A1, TSP_1:def_2; ::_thesis: F0 = F /\ the carrier of X0 thus F0 = F /\ the carrier of X0 ; ::_thesis: verum end; assume A2: F = MaxADSet F ; ::_thesis: ( for F0 being Subset of X0 holds ( not F0 is closed or not F0 = F /\ the carrier of X0 ) or F is closed ) given F0 being Subset of X0 such that A3: F0 is closed and A4: F0 = F /\ the carrier of X0 ; ::_thesis: F is closed set E = F0; F0 c= M ; then reconsider E = F0 as Subset of X by XBOOLE_1:1; A5: E c= MaxADSet F by A2, A4, XBOOLE_1:17; A6: M is maximal_T_0 by Th11; for x being set st x in F holds x in MaxADSet E proof let x be set ; ::_thesis: ( x in F implies x in MaxADSet E ) assume A7: x in F ; ::_thesis: x in MaxADSet E then reconsider a = x as Point of X ; consider b being Point of X such that A8: b in M and A9: M /\ (MaxADSet a) = {b} by A6, Def6; A10: {b} c= MaxADSet a by A9, XBOOLE_1:17; {a} c= F by A7, ZFMISC_1:31; then MaxADSet {a} c= F by A2, TEX_4:34; then MaxADSet a c= F by TEX_4:28; then {b} c= F by A10, XBOOLE_1:1; then b in F by ZFMISC_1:31; then b in E by A4, A8, XBOOLE_0:def_4; then {b} c= E by ZFMISC_1:31; then MaxADSet {b} c= MaxADSet E by TEX_4:31; then A11: MaxADSet b c= MaxADSet E by TEX_4:28; b in MaxADSet a by A10, ZFMISC_1:31; then MaxADSet b = MaxADSet a by TEX_4:21; then {a} c= MaxADSet b by TEX_4:18; then a in MaxADSet b by ZFMISC_1:31; hence x in MaxADSet E by A11; ::_thesis: verum end; then A12: F c= MaxADSet E by TARSKI:def_3; MaxADSet E is closed by A3, Th16; hence F is closed by A2, A5, A12, TEX_4:35; ::_thesis: verum end; begin theorem Th18: :: TSP_2:18 for X being non empty TopSpace for X0 being non empty maximal_Kolmogorov_subspace of X for r being Function of X,X0 for M being Subset of X st M = the carrier of X0 & ( for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) holds r is continuous Function of X,X0 proof let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X for r being Function of X,X0 for M being Subset of X st M = the carrier of X0 & ( for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) holds r is continuous Function of X,X0 let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for r being Function of X,X0 for M being Subset of X st M = the carrier of X0 & ( for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) holds r is continuous Function of X,X0 let r be Function of X,X0; ::_thesis: for M being Subset of X st M = the carrier of X0 & ( for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) holds r is continuous Function of X,X0 let M be Subset of X; ::_thesis: ( M = the carrier of X0 & ( for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) implies r is continuous Function of X,X0 ) assume A1: M = the carrier of X0 ; ::_thesis: ( ex a being Point of X st not M /\ (MaxADSet a) = {(r . a)} or r is continuous Function of X,X0 ) reconsider N = M as Subset of X ; assume A2: for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ; ::_thesis: r is continuous Function of X,X0 A3: N is maximal_T_0 by A1, Th11; then A4: N is T_0 by Def4; for F being Subset of X0 st F is closed holds r " F is closed proof let F be Subset of X0; ::_thesis: ( F is closed implies r " F is closed ) reconsider E = F as Subset of X by A1, XBOOLE_1:1; set R = { (MaxADSet a) where a is Point of X : a in E } ; now__::_thesis:_for_x_being_set_st_x_in_r_"_F_holds_ x_in_union__{__(MaxADSet_a)_where_a_is_Point_of_X_:_a_in_E__}_ let x be set ; ::_thesis: ( x in r " F implies x in union { (MaxADSet a) where a is Point of X : a in E } ) assume A5: x in r " F ; ::_thesis: x in union { (MaxADSet a) where a is Point of X : a in E } then reconsider b = x as Point of X ; A6: r . b in F by A5, FUNCT_2:38; E c= the carrier of X ; then reconsider a = r . b as Point of X by A6; MaxADSet a in { (MaxADSet a) where a is Point of X : a in E } by A6; then A7: MaxADSet a c= union { (MaxADSet a) where a is Point of X : a in E } by ZFMISC_1:74; M /\ (MaxADSet b) = {a} by A2; then a in M /\ (MaxADSet b) by ZFMISC_1:31; then a in MaxADSet b by XBOOLE_0:def_4; then A8: MaxADSet a = MaxADSet b by TEX_4:21; A9: {b} c= MaxADSet b by TEX_4:18; b in {b} by TARSKI:def_1; then b in MaxADSet a by A8, A9; hence x in union { (MaxADSet a) where a is Point of X : a in E } by A7; ::_thesis: verum end; then A10: r " F c= union { (MaxADSet a) where a is Point of X : a in E } by TARSKI:def_3; assume F is closed ; ::_thesis: r " F is closed then ex P being Subset of X st ( P is closed & P /\ ([#] X0) = F ) by PRE_TOPC:13; then A11: MaxADSet E is closed by A1, A3, Th5; now__::_thesis:_for_C_being_set_st_C_in__{__(MaxADSet_a)_where_a_is_Point_of_X_:_a_in_E__}__holds_ C_c=_r_"_F let C be set ; ::_thesis: ( C in { (MaxADSet a) where a is Point of X : a in E } implies C c= r " F ) assume C in { (MaxADSet a) where a is Point of X : a in E } ; ::_thesis: C c= r " F then consider a being Point of X such that A12: C = MaxADSet a and A13: a in E ; now__::_thesis:_for_x_being_set_st_x_in_C_holds_ x_in_r_"_F let x be set ; ::_thesis: ( x in C implies x in r " F ) assume A14: x in C ; ::_thesis: x in r " F then reconsider b = x as Point of X by A12; A15: M /\ (MaxADSet b) = {(r . b)} by A2; A16: M /\ (MaxADSet a) = {a} by A1, A4, A13, Def2; MaxADSet a = MaxADSet b by A12, A14, TEX_4:21; then a = r . x by A16, A15, ZFMISC_1:3; hence x in r " F by A12, A13, A14, FUNCT_2:38; ::_thesis: verum end; hence C c= r " F by TARSKI:def_3; ::_thesis: verum end; then A17: union { (MaxADSet a) where a is Point of X : a in E } c= r " F by ZFMISC_1:76; union { (MaxADSet a) where a is Point of X : a in E } = MaxADSet E by TEX_4:def_11; hence r " F is closed by A11, A17, A10, XBOOLE_0:def_10; ::_thesis: verum end; hence r is continuous Function of X,X0 by PRE_TOPC:def_6; ::_thesis: verum end; theorem :: TSP_2:19 for X being non empty TopSpace for X0 being non empty maximal_Kolmogorov_subspace of X for r being Function of X,X0 st ( for a being Point of X holds r . a in MaxADSet a ) holds r is continuous Function of X,X0 proof let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X for r being Function of X,X0 st ( for a being Point of X holds r . a in MaxADSet a ) holds r is continuous Function of X,X0 let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for r being Function of X,X0 st ( for a being Point of X holds r . a in MaxADSet a ) holds r is continuous Function of X,X0 let r be Function of X,X0; ::_thesis: ( ( for a being Point of X holds r . a in MaxADSet a ) implies r is continuous Function of X,X0 ) reconsider M = the carrier of X0 as Subset of X by TSEP_1:1; assume A1: for a being Point of X holds r . a in MaxADSet a ; ::_thesis: r is continuous Function of X,X0 M is maximal_T_0 by Th11; then A2: M is T_0 by Def4; A3: M c= the carrier of X ; for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} proof let a be Point of X; ::_thesis: M /\ (MaxADSet a) = {(r . a)} reconsider s = r . a as Point of X by A3, TARSKI:def_3; A4: s in MaxADSet a by A1; M /\ (MaxADSet s) = {s} by A2, Def2; hence M /\ (MaxADSet a) = {(r . a)} by A4, TEX_4:21; ::_thesis: verum end; hence r is continuous Function of X,X0 by Th18; ::_thesis: verum end; theorem Th20: :: TSP_2:20 for X being non empty TopSpace for X0 being non empty maximal_Kolmogorov_subspace of X for r being continuous Function of X,X0 for M being Subset of X st M = the carrier of X0 & ( for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) holds r is being_a_retraction proof let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X for r being continuous Function of X,X0 for M being Subset of X st M = the carrier of X0 & ( for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) holds r is being_a_retraction let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for r being continuous Function of X,X0 for M being Subset of X st M = the carrier of X0 & ( for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) holds r is being_a_retraction let r be continuous Function of X,X0; ::_thesis: for M being Subset of X st M = the carrier of X0 & ( for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) holds r is being_a_retraction let M be Subset of X; ::_thesis: ( M = the carrier of X0 & ( for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) implies r is being_a_retraction ) reconsider N = M as Subset of X ; assume A1: M = the carrier of X0 ; ::_thesis: ( ex a being Point of X st not M /\ (MaxADSet a) = {(r . a)} or r is being_a_retraction ) then N is maximal_T_0 by Th11; then A2: N is T_0 by Def4; assume A3: for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ; ::_thesis: r is being_a_retraction for x being Point of X st x in the carrier of X0 holds r . x = x proof let x be Point of X; ::_thesis: ( x in the carrier of X0 implies r . x = x ) assume x in the carrier of X0 ; ::_thesis: r . x = x then A4: M /\ (MaxADSet x) = {x} by A1, A2, Def2; M /\ (MaxADSet x) = {(r . x)} by A3; hence r . x = x by A4, ZFMISC_1:3; ::_thesis: verum end; hence r is being_a_retraction by BORSUK_1:def_16; ::_thesis: verum end; theorem Th21: :: TSP_2:21 for X being non empty TopSpace for X0 being non empty maximal_Kolmogorov_subspace of X for r being continuous Function of X,X0 st ( for a being Point of X holds r . a in MaxADSet a ) holds r is being_a_retraction proof let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X for r being continuous Function of X,X0 st ( for a being Point of X holds r . a in MaxADSet a ) holds r is being_a_retraction let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for r being continuous Function of X,X0 st ( for a being Point of X holds r . a in MaxADSet a ) holds r is being_a_retraction let r be continuous Function of X,X0; ::_thesis: ( ( for a being Point of X holds r . a in MaxADSet a ) implies r is being_a_retraction ) reconsider M = the carrier of X0 as Subset of X by TSEP_1:1; assume A1: for a being Point of X holds r . a in MaxADSet a ; ::_thesis: r is being_a_retraction M is maximal_T_0 by Th11; then A2: M is T_0 by Def4; A3: M c= the carrier of X ; for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} proof let a be Point of X; ::_thesis: M /\ (MaxADSet a) = {(r . a)} reconsider s = r . a as Point of X by A3, TARSKI:def_3; A4: s in MaxADSet a by A1; M /\ (MaxADSet s) = {s} by A2, Def2; hence M /\ (MaxADSet a) = {(r . a)} by A4, TEX_4:21; ::_thesis: verum end; hence r is being_a_retraction by Th20; ::_thesis: verum end; theorem Th22: :: TSP_2:22 for X being non empty TopSpace for X0 being non empty maximal_Kolmogorov_subspace of X ex r being continuous Function of X,X0 st r is being_a_retraction proof let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X ex r being continuous Function of X,X0 st r is being_a_retraction let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: ex r being continuous Function of X,X0 st r is being_a_retraction reconsider M = the carrier of X0 as Subset of X by TSEP_1:1; defpred S1[ Point of X, set ] means M /\ (MaxADSet $1) = {$2}; A1: M is maximal_T_0 by Th11; A2: for x being Point of X ex a being Point of X0 st S1[x,a] proof let x be Point of X; ::_thesis: ex a being Point of X0 st S1[x,a] consider a being Point of X such that A3: a in M and A4: M /\ (MaxADSet x) = {a} by A1, Def6; reconsider a = a as Point of X0 by A3; take a ; ::_thesis: S1[x,a] thus S1[x,a] by A4; ::_thesis: verum end; consider r being Function of X,X0 such that A5: for x being Point of X holds S1[x,r . x] from FUNCT_2:sch_3(A2); reconsider r = r as continuous Function of X,X0 by A5, Th18; take r ; ::_thesis: r is being_a_retraction thus r is being_a_retraction by A5, Th20; ::_thesis: verum end; theorem :: TSP_2:23 for X being non empty TopSpace for X0 being non empty maximal_Kolmogorov_subspace of X holds X0 is_a_retract_of X proof let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X holds X0 is_a_retract_of X let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: X0 is_a_retract_of X ex r being continuous Function of X,X0 st r is being_a_retraction by Th22; hence X0 is_a_retract_of X by BORSUK_1:def_17; ::_thesis: verum end; Lm2: for X being non empty TopSpace for X0 being non empty maximal_Kolmogorov_subspace of X for r being continuous Function of X,X0 st r is being_a_retraction holds for a being Point of X for b being Point of X0 st a = b holds r " (Cl {b}) = Cl {a} proof let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X for r being continuous Function of X,X0 st r is being_a_retraction holds for a being Point of X for b being Point of X0 st a = b holds r " (Cl {b}) = Cl {a} let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for r being continuous Function of X,X0 st r is being_a_retraction holds for a being Point of X for b being Point of X0 st a = b holds r " (Cl {b}) = Cl {a} let r be continuous Function of X,X0; ::_thesis: ( r is being_a_retraction implies for a being Point of X for b being Point of X0 st a = b holds r " (Cl {b}) = Cl {a} ) assume A1: r is being_a_retraction ; ::_thesis: for a being Point of X for b being Point of X0 st a = b holds r " (Cl {b}) = Cl {a} reconsider A = the carrier of X0 as Subset of X by TSEP_1:1; let a be Point of X; ::_thesis: for b being Point of X0 st a = b holds r " (Cl {b}) = Cl {a} let b be Point of X0; ::_thesis: ( a = b implies r " (Cl {b}) = Cl {a} ) A2: b in {b} by TARSKI:def_1; assume A3: a = b ; ::_thesis: r " (Cl {b}) = Cl {a} then r . a = b by A1, BORSUK_1:def_16; then A4: a in r " {b} by A2, FUNCT_2:38; A5: A is maximal_T_0 by Th11; A6: r " (Cl {b}) c= Cl {a} proof assume not r " (Cl {b}) c= Cl {a} ; ::_thesis: contradiction then consider c being set such that A7: c in r " (Cl {b}) and A8: not c in Cl {a} by TARSKI:def_3; reconsider c = c as Point of X by A7; consider d being Point of X such that A9: d in A and A10: A /\ (MaxADSet c) = {d} by A5, Def6; A11: {d} c= MaxADSet c by A10, XBOOLE_1:17; r " (Cl {b}) is closed by PRE_TOPC:def_6; then MaxADSet c c= r " (Cl {b}) by A7, TEX_4:23; then {d} c= r " (Cl {b}) by A11, XBOOLE_1:1; then A12: d in r " (Cl {b}) by ZFMISC_1:31; reconsider e = d as Point of X0 by A9; {c} c= MaxADSet c by TEX_4:18; then A13: c in MaxADSet c by ZFMISC_1:31; A14: Cl {b} c= Cl {a} by A3, TOPS_3:53; r . d = e by A1, BORSUK_1:def_16; then e in Cl {b} by A12, FUNCT_2:38; then A15: MaxADSet d c= Cl {a} by A14, TEX_4:23; d in MaxADSet c by A11, ZFMISC_1:31; then MaxADSet d = MaxADSet c by TEX_4:21; hence contradiction by A8, A13, A15; ::_thesis: verum end; A16: r " (Cl {b}) is closed by PRE_TOPC:def_6; r " {b} c= r " (Cl {b}) by PRE_TOPC:18, RELAT_1:143; then {a} c= r " (Cl {b}) by A4, ZFMISC_1:31; then Cl {a} c= r " (Cl {b}) by A16, TOPS_1:5; hence r " (Cl {b}) = Cl {a} by A6, XBOOLE_0:def_10; ::_thesis: verum end; Lm3: for X being non empty TopSpace for X0 being non empty maximal_Kolmogorov_subspace of X for r being continuous Function of X,X0 st r is being_a_retraction holds for A being Subset of X st A = the carrier of X0 holds for a being Point of X holds A /\ (MaxADSet a) = {(r . a)} proof let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X for r being continuous Function of X,X0 st r is being_a_retraction holds for A being Subset of X st A = the carrier of X0 holds for a being Point of X holds A /\ (MaxADSet a) = {(r . a)} let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for r being continuous Function of X,X0 st r is being_a_retraction holds for A being Subset of X st A = the carrier of X0 holds for a being Point of X holds A /\ (MaxADSet a) = {(r . a)} let r be continuous Function of X,X0; ::_thesis: ( r is being_a_retraction implies for A being Subset of X st A = the carrier of X0 holds for a being Point of X holds A /\ (MaxADSet a) = {(r . a)} ) assume A1: r is being_a_retraction ; ::_thesis: for A being Subset of X st A = the carrier of X0 holds for a being Point of X holds A /\ (MaxADSet a) = {(r . a)} let A be Subset of X; ::_thesis: ( A = the carrier of X0 implies for a being Point of X holds A /\ (MaxADSet a) = {(r . a)} ) reconsider N = A as Subset of X ; assume A2: A = the carrier of X0 ; ::_thesis: for a being Point of X holds A /\ (MaxADSet a) = {(r . a)} let a be Point of X; ::_thesis: A /\ (MaxADSet a) = {(r . a)} A3: N is maximal_T_0 by A2, Th11; then consider c being Point of X such that A4: c in A and A5: A /\ (MaxADSet a) = {c} by Def6; A6: {c} c= MaxADSet c by TEX_4:18; r . a in A by A2; then reconsider d = r . a as Point of X ; {(r . a)} c= Cl {(r . a)} by PRE_TOPC:18; then A7: r . a in Cl {(r . a)} by ZFMISC_1:31; {c} c= MaxADSet a by A5, XBOOLE_1:17; then c in MaxADSet a by ZFMISC_1:31; then A8: MaxADSet c = MaxADSet a by TEX_4:21; reconsider b = c as Point of X0 by A2, A4; A9: {a} c= MaxADSet a by TEX_4:18; A10: r " (Cl {b}) = Cl {c} by A1, Lm2; then {c} c= r " (Cl {b}) by PRE_TOPC:18; then c in r " (Cl {b}) by ZFMISC_1:31; then MaxADSet a c= r " (Cl {b}) by A10, A8, TEX_4:23; then {a} c= r " (Cl {b}) by A9, XBOOLE_1:1; then a in r " (Cl {b}) by ZFMISC_1:31; then A11: r . a in Cl {b} by FUNCT_2:38; r " (Cl {(r . a)}) = Cl {d} by A1, Lm2; then a in Cl {d} by A7, FUNCT_2:38; then MaxADSet c c= Cl {d} by A8, TEX_4:23; then {c} c= Cl {d} by A6, XBOOLE_1:1; then A12: Cl {c} c= Cl {d} by TOPS_1:5; Cl {b} c= Cl {c} by TOPS_3:53; then {d} c= Cl {c} by A11, ZFMISC_1:31; then Cl {d} c= Cl {c} by TOPS_1:5; then Cl {d} = Cl {c} by A12, XBOOLE_0:def_10; then A13: MaxADSet d = MaxADSet a by A8, TEX_4:49; N is T_0 by A3, Def4; hence A /\ (MaxADSet a) = {(r . a)} by A2, A13, Def2; ::_thesis: verum end; Lm4: for X being non empty TopSpace for X0 being non empty maximal_Kolmogorov_subspace of X for r being continuous Function of X,X0 st r is being_a_retraction holds for a being Point of X for b being Point of X0 st a = b holds MaxADSet a c= r " {b} proof let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X for r being continuous Function of X,X0 st r is being_a_retraction holds for a being Point of X for b being Point of X0 st a = b holds MaxADSet a c= r " {b} let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for r being continuous Function of X,X0 st r is being_a_retraction holds for a being Point of X for b being Point of X0 st a = b holds MaxADSet a c= r " {b} let r be continuous Function of X,X0; ::_thesis: ( r is being_a_retraction implies for a being Point of X for b being Point of X0 st a = b holds MaxADSet a c= r " {b} ) assume A1: r is being_a_retraction ; ::_thesis: for a being Point of X for b being Point of X0 st a = b holds MaxADSet a c= r " {b} reconsider A = the carrier of X0 as Subset of X by TSEP_1:1; let a be Point of X; ::_thesis: for b being Point of X0 st a = b holds MaxADSet a c= r " {b} let b be Point of X0; ::_thesis: ( a = b implies MaxADSet a c= r " {b} ) assume A2: a = b ; ::_thesis: MaxADSet a c= r " {b} assume not MaxADSet a c= r " {b} ; ::_thesis: contradiction then consider s being set such that A3: s in MaxADSet a and A4: not s in r " {b} by TARSKI:def_3; reconsider s = s as Point of X by A3; A5: MaxADSet a = MaxADSet s by A3, TEX_4:21; A6: {s} c= MaxADSet s by TEX_4:18; A7: r " (Cl {b}) = Cl {a} by A1, A2, Lm2; then {a} c= r " (Cl {b}) by PRE_TOPC:18; then a in r " (Cl {b}) by ZFMISC_1:31; then MaxADSet s c= r " (Cl {b}) by A7, A5, TEX_4:23; then {s} c= r " (Cl {b}) by A6, XBOOLE_1:1; then s in r " (Cl {b}) by ZFMISC_1:31; then A8: r . s in Cl {b} by FUNCT_2:38; A c= the carrier of X ; then reconsider d = r . s as Point of X by TARSKI:def_3; {(r . s)} c= Cl {(r . s)} by PRE_TOPC:18; then A9: r . s in Cl {(r . s)} by ZFMISC_1:31; A10: {a} c= MaxADSet a by TEX_4:18; r " (Cl {(r . s)}) = Cl {d} by A1, Lm2; then s in Cl {d} by A9, FUNCT_2:38; then MaxADSet a c= Cl {d} by A5, TEX_4:23; then {a} c= Cl {d} by A10, XBOOLE_1:1; then A11: Cl {a} c= Cl {d} by TOPS_1:5; Cl {b} c= Cl {a} by A2, TOPS_3:53; then {d} c= Cl {a} by A8, ZFMISC_1:31; then Cl {d} c= Cl {a} by TOPS_1:5; then Cl {d} = Cl {a} by A11, XBOOLE_0:def_10; then A12: MaxADSet d = MaxADSet a by TEX_4:49; A is maximal_T_0 by Th11; then A13: A is T_0 by Def4; r . a = b by A1, A2, BORSUK_1:def_16; then A /\ (MaxADSet a) = {b} by A1, Lm3; then {b} = {(r . s)} by A13, A12, Def2; then r . s in {b} by ZFMISC_1:31; hence contradiction by A4, FUNCT_2:38; ::_thesis: verum end; Lm5: for X being non empty TopSpace for X0 being non empty maximal_Kolmogorov_subspace of X for r being continuous Function of X,X0 st r is being_a_retraction holds for a being Point of X for b being Point of X0 st a = b holds r " {b} = MaxADSet a proof let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X for r being continuous Function of X,X0 st r is being_a_retraction holds for a being Point of X for b being Point of X0 st a = b holds r " {b} = MaxADSet a let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for r being continuous Function of X,X0 st r is being_a_retraction holds for a being Point of X for b being Point of X0 st a = b holds r " {b} = MaxADSet a let r be continuous Function of X,X0; ::_thesis: ( r is being_a_retraction implies for a being Point of X for b being Point of X0 st a = b holds r " {b} = MaxADSet a ) assume A1: r is being_a_retraction ; ::_thesis: for a being Point of X for b being Point of X0 st a = b holds r " {b} = MaxADSet a reconsider A = the carrier of X0 as Subset of X by TSEP_1:1; let a be Point of X; ::_thesis: for b being Point of X0 st a = b holds r " {b} = MaxADSet a let b be Point of X0; ::_thesis: ( a = b implies r " {b} = MaxADSet a ) assume A2: a = b ; ::_thesis: r " {b} = MaxADSet a A3: r " {b} c= MaxADSet a proof assume not r " {b} c= MaxADSet a ; ::_thesis: contradiction then consider s being set such that A4: s in r " {b} and A5: not s in MaxADSet a by TARSKI:def_3; reconsider s = s as Point of X by A4; r . s in {b} by A4, FUNCT_2:38; then {(r . s)} c= {b} by ZFMISC_1:31; then {(r . s)} = {b} by ZFMISC_1:18; then A /\ (MaxADSet s) = {b} by A1, Lm3; then {a} c= MaxADSet s by A2, XBOOLE_1:17; then a in MaxADSet s by ZFMISC_1:31; then A6: MaxADSet s = MaxADSet a by TEX_4:21; {s} c= MaxADSet s by TEX_4:18; hence contradiction by A5, A6, ZFMISC_1:31; ::_thesis: verum end; MaxADSet a c= r " {b} by A1, A2, Lm4; hence r " {b} = MaxADSet a by A3, XBOOLE_0:def_10; ::_thesis: verum end; Lm6: for X being non empty TopSpace for X0 being non empty maximal_Kolmogorov_subspace of X for r being continuous Function of X,X0 st r is being_a_retraction holds for E being Subset of X for F being Subset of X0 st F = E holds r " F = MaxADSet E proof let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X for r being continuous Function of X,X0 st r is being_a_retraction holds for E being Subset of X for F being Subset of X0 st F = E holds r " F = MaxADSet E let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for r being continuous Function of X,X0 st r is being_a_retraction holds for E being Subset of X for F being Subset of X0 st F = E holds r " F = MaxADSet E let r be continuous Function of X,X0; ::_thesis: ( r is being_a_retraction implies for E being Subset of X for F being Subset of X0 st F = E holds r " F = MaxADSet E ) assume A1: r is being_a_retraction ; ::_thesis: for E being Subset of X for F being Subset of X0 st F = E holds r " F = MaxADSet E reconsider A = the carrier of X0 as Subset of X by TSEP_1:1; let E be Subset of X; ::_thesis: for F being Subset of X0 st F = E holds r " F = MaxADSet E let F be Subset of X0; ::_thesis: ( F = E implies r " F = MaxADSet E ) set R = { (MaxADSet a) where a is Point of X : a in E } ; assume A2: F = E ; ::_thesis: r " F = MaxADSet E now__::_thesis:_for_x_being_set_st_x_in_r_"_F_holds_ x_in_union__{__(MaxADSet_a)_where_a_is_Point_of_X_:_a_in_E__}_ let x be set ; ::_thesis: ( x in r " F implies x in union { (MaxADSet a) where a is Point of X : a in E } ) assume A3: x in r " F ; ::_thesis: x in union { (MaxADSet a) where a is Point of X : a in E } then reconsider b = x as Point of X ; A4: r . b in F by A3, FUNCT_2:38; then reconsider a = r . b as Point of X by A2; MaxADSet a in { (MaxADSet a) where a is Point of X : a in E } by A2, A4; then A5: MaxADSet a c= union { (MaxADSet a) where a is Point of X : a in E } by ZFMISC_1:74; A /\ (MaxADSet b) = {a} by A1, Lm3; then a in A /\ (MaxADSet b) by ZFMISC_1:31; then a in MaxADSet b by XBOOLE_0:def_4; then A6: MaxADSet a = MaxADSet b by TEX_4:21; {b} c= MaxADSet b by TEX_4:18; then b in MaxADSet a by A6, ZFMISC_1:31; hence x in union { (MaxADSet a) where a is Point of X : a in E } by A5; ::_thesis: verum end; then A7: r " F c= union { (MaxADSet a) where a is Point of X : a in E } by TARSKI:def_3; A is maximal_T_0 by Th11; then A8: A is T_0 by Def4; now__::_thesis:_for_C_being_set_st_C_in__{__(MaxADSet_a)_where_a_is_Point_of_X_:_a_in_E__}__holds_ C_c=_r_"_F let C be set ; ::_thesis: ( C in { (MaxADSet a) where a is Point of X : a in E } implies C c= r " F ) assume C in { (MaxADSet a) where a is Point of X : a in E } ; ::_thesis: C c= r " F then consider a being Point of X such that A9: C = MaxADSet a and A10: a in E ; now__::_thesis:_for_x_being_set_st_x_in_C_holds_ x_in_r_"_F let x be set ; ::_thesis: ( x in C implies x in r " F ) assume A11: x in C ; ::_thesis: x in r " F then reconsider b = x as Point of X by A9; A12: A /\ (MaxADSet b) = {(r . b)} by A1, Lm3; A13: A /\ (MaxADSet a) = {a} by A2, A8, A10, Def2; MaxADSet a = MaxADSet b by A9, A11, TEX_4:21; then a = r . x by A13, A12, ZFMISC_1:3; hence x in r " F by A2, A9, A10, A11, FUNCT_2:38; ::_thesis: verum end; hence C c= r " F by TARSKI:def_3; ::_thesis: verum end; then A14: union { (MaxADSet a) where a is Point of X : a in E } c= r " F by ZFMISC_1:76; MaxADSet E = union { (MaxADSet a) where a is Point of X : a in E } by TEX_4:def_11; hence r " F = MaxADSet E by A14, A7, XBOOLE_0:def_10; ::_thesis: verum end; definition let X be non empty TopSpace; let X0 be non empty maximal_Kolmogorov_subspace of X; func Stone-retraction (X,X0) -> continuous Function of X,X0 means :Def9: :: TSP_2:def 9 it is being_a_retraction ; existence ex b1 being continuous Function of X,X0 st b1 is being_a_retraction by Th22; uniqueness for b1, b2 being continuous Function of X,X0 st b1 is being_a_retraction & b2 is being_a_retraction holds b1 = b2 proof reconsider M = the carrier of X0 as non empty Subset of X by TSEP_1:1; let r1, r2 be continuous Function of X,X0; ::_thesis: ( r1 is being_a_retraction & r2 is being_a_retraction implies r1 = r2 ) assume that A1: r1 is being_a_retraction and A2: r2 is being_a_retraction ; ::_thesis: r1 = r2 for x being set st x in the carrier of X holds r1 . x = r2 . x proof let x be set ; ::_thesis: ( x in the carrier of X implies r1 . x = r2 . x ) assume x in the carrier of X ; ::_thesis: r1 . x = r2 . x then reconsider a = x as Point of X ; A3: M /\ (MaxADSet a) = {(r2 . a)} by A2, Lm3; M /\ (MaxADSet a) = {(r1 . a)} by A1, Lm3; hence r1 . x = r2 . x by A3, ZFMISC_1:3; ::_thesis: verum end; hence r1 = r2 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def9 defines Stone-retraction TSP_2:def_9_:_ for X being non empty TopSpace for X0 being non empty maximal_Kolmogorov_subspace of X for b3 being continuous Function of X,X0 holds ( b3 = Stone-retraction (X,X0) iff b3 is being_a_retraction ); theorem :: TSP_2:24 for X being non empty TopSpace for X0 being non empty maximal_Kolmogorov_subspace of X for a being Point of X for b being Point of X0 st a = b holds (Stone-retraction (X,X0)) " (Cl {b}) = Cl {a} proof let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X for a being Point of X for b being Point of X0 st a = b holds (Stone-retraction (X,X0)) " (Cl {b}) = Cl {a} let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for a being Point of X for b being Point of X0 st a = b holds (Stone-retraction (X,X0)) " (Cl {b}) = Cl {a} let a be Point of X; ::_thesis: for b being Point of X0 st a = b holds (Stone-retraction (X,X0)) " (Cl {b}) = Cl {a} let b be Point of X0; ::_thesis: ( a = b implies (Stone-retraction (X,X0)) " (Cl {b}) = Cl {a} ) assume A1: a = b ; ::_thesis: (Stone-retraction (X,X0)) " (Cl {b}) = Cl {a} Stone-retraction (X,X0) is being_a_retraction by Def9; hence (Stone-retraction (X,X0)) " (Cl {b}) = Cl {a} by A1, Lm2; ::_thesis: verum end; theorem Th25: :: TSP_2:25 for X being non empty TopSpace for X0 being non empty maximal_Kolmogorov_subspace of X for a being Point of X for b being Point of X0 st a = b holds (Stone-retraction (X,X0)) " {b} = MaxADSet a proof let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X for a being Point of X for b being Point of X0 st a = b holds (Stone-retraction (X,X0)) " {b} = MaxADSet a let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for a being Point of X for b being Point of X0 st a = b holds (Stone-retraction (X,X0)) " {b} = MaxADSet a let a be Point of X; ::_thesis: for b being Point of X0 st a = b holds (Stone-retraction (X,X0)) " {b} = MaxADSet a let b be Point of X0; ::_thesis: ( a = b implies (Stone-retraction (X,X0)) " {b} = MaxADSet a ) assume A1: a = b ; ::_thesis: (Stone-retraction (X,X0)) " {b} = MaxADSet a Stone-retraction (X,X0) is being_a_retraction by Def9; hence (Stone-retraction (X,X0)) " {b} = MaxADSet a by A1, Lm5; ::_thesis: verum end; theorem Th26: :: TSP_2:26 for X being non empty TopSpace for X0 being non empty maximal_Kolmogorov_subspace of X for E being Subset of X for F being Subset of X0 st F = E holds (Stone-retraction (X,X0)) " F = MaxADSet E proof let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X for E being Subset of X for F being Subset of X0 st F = E holds (Stone-retraction (X,X0)) " F = MaxADSet E let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for E being Subset of X for F being Subset of X0 st F = E holds (Stone-retraction (X,X0)) " F = MaxADSet E let E be Subset of X; ::_thesis: for F being Subset of X0 st F = E holds (Stone-retraction (X,X0)) " F = MaxADSet E let F be Subset of X0; ::_thesis: ( F = E implies (Stone-retraction (X,X0)) " F = MaxADSet E ) assume A1: F = E ; ::_thesis: (Stone-retraction (X,X0)) " F = MaxADSet E Stone-retraction (X,X0) is being_a_retraction by Def9; hence (Stone-retraction (X,X0)) " F = MaxADSet E by A1, Lm6; ::_thesis: verum end; definition let X be non empty TopSpace; let X0 be non empty maximal_Kolmogorov_subspace of X; redefine func Stone-retraction (X,X0) means :Def10: :: TSP_2:def 10 for M being Subset of X st M = the carrier of X0 holds for a being Point of X holds M /\ (MaxADSet a) = {(it . a)}; compatibility for b1 being continuous Function of X,X0 holds ( b1 = Stone-retraction (X,X0) iff for M being Subset of X st M = the carrier of X0 holds for a being Point of X holds M /\ (MaxADSet a) = {(b1 . a)} ) proof reconsider M = the carrier of X0 as Subset of X by TSEP_1:1; let r be continuous Function of X,X0; ::_thesis: ( r = Stone-retraction (X,X0) iff for M being Subset of X st M = the carrier of X0 holds for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) thus ( r = Stone-retraction (X,X0) implies for M being Subset of X st M = the carrier of X0 holds for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) ::_thesis: ( ( for M being Subset of X st M = the carrier of X0 holds for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) implies r = Stone-retraction (X,X0) ) proof assume A1: r = Stone-retraction (X,X0) ; ::_thesis: for M being Subset of X st M = the carrier of X0 holds for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} let M be Subset of X; ::_thesis: ( M = the carrier of X0 implies for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) A2: Stone-retraction (X,X0) is being_a_retraction by Def9; assume M = the carrier of X0 ; ::_thesis: for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} hence for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} by A1, A2, Lm3; ::_thesis: verum end; assume for A being Subset of X st A = the carrier of X0 holds for a being Point of X holds A /\ (MaxADSet a) = {(r . a)} ; ::_thesis: r = Stone-retraction (X,X0) then for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ; then r is being_a_retraction by Th20; hence r = Stone-retraction (X,X0) by Def9; ::_thesis: verum end; end; :: deftheorem Def10 defines Stone-retraction TSP_2:def_10_:_ for X being non empty TopSpace for X0 being non empty maximal_Kolmogorov_subspace of X for b3 being continuous Function of X,X0 holds ( b3 = Stone-retraction (X,X0) iff for M being Subset of X st M = the carrier of X0 holds for a being Point of X holds M /\ (MaxADSet a) = {(b3 . a)} ); definition let X be non empty TopSpace; let X0 be non empty maximal_Kolmogorov_subspace of X; redefine func Stone-retraction (X,X0) means :Def11: :: TSP_2:def 11 for a being Point of X holds it . a in MaxADSet a; compatibility for b1 being continuous Function of X,X0 holds ( b1 = Stone-retraction (X,X0) iff for a being Point of X holds b1 . a in MaxADSet a ) proof reconsider A = the carrier of X0 as Subset of X by TSEP_1:1; let r be continuous Function of X,X0; ::_thesis: ( r = Stone-retraction (X,X0) iff for a being Point of X holds r . a in MaxADSet a ) thus ( r = Stone-retraction (X,X0) implies for a being Point of X holds r . a in MaxADSet a ) ::_thesis: ( ( for a being Point of X holds r . a in MaxADSet a ) implies r = Stone-retraction (X,X0) ) proof assume A1: r = Stone-retraction (X,X0) ; ::_thesis: for a being Point of X holds r . a in MaxADSet a let a be Point of X; ::_thesis: r . a in MaxADSet a A /\ (MaxADSet a) = {(r . a)} by A1, Def10; then {(r . a)} c= MaxADSet a by XBOOLE_1:17; hence r . a in MaxADSet a by ZFMISC_1:31; ::_thesis: verum end; assume for a being Point of X holds r . a in MaxADSet a ; ::_thesis: r = Stone-retraction (X,X0) then r is being_a_retraction by Th21; hence r = Stone-retraction (X,X0) by Def9; ::_thesis: verum end; end; :: deftheorem Def11 defines Stone-retraction TSP_2:def_11_:_ for X being non empty TopSpace for X0 being non empty maximal_Kolmogorov_subspace of X for b3 being continuous Function of X,X0 holds ( b3 = Stone-retraction (X,X0) iff for a being Point of X holds b3 . a in MaxADSet a ); theorem Th27: :: TSP_2:27 for X being non empty TopSpace for X0 being non empty maximal_Kolmogorov_subspace of X for a being Point of X holds (Stone-retraction (X,X0)) " {((Stone-retraction (X,X0)) . a)} = MaxADSet a proof let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X for a being Point of X holds (Stone-retraction (X,X0)) " {((Stone-retraction (X,X0)) . a)} = MaxADSet a let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for a being Point of X holds (Stone-retraction (X,X0)) " {((Stone-retraction (X,X0)) . a)} = MaxADSet a let a be Point of X; ::_thesis: (Stone-retraction (X,X0)) " {((Stone-retraction (X,X0)) . a)} = MaxADSet a reconsider A = the carrier of X0 as Subset of X by TSEP_1:1; set r = Stone-retraction (X,X0); (Stone-retraction (X,X0)) . a in A ; then reconsider b = (Stone-retraction (X,X0)) . a as Point of X ; A1: (Stone-retraction (X,X0)) . a in MaxADSet a by Def11; (Stone-retraction (X,X0)) " {((Stone-retraction (X,X0)) . a)} = MaxADSet b by Th25; hence (Stone-retraction (X,X0)) " {((Stone-retraction (X,X0)) . a)} = MaxADSet a by A1, TEX_4:21; ::_thesis: verum end; theorem :: TSP_2:28 for X being non empty TopSpace for X0 being non empty maximal_Kolmogorov_subspace of X for a being Point of X holds Im ((Stone-retraction (X,X0)),a) = (Stone-retraction (X,X0)) .: (MaxADSet a) proof let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X for a being Point of X holds Im ((Stone-retraction (X,X0)),a) = (Stone-retraction (X,X0)) .: (MaxADSet a) let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for a being Point of X holds Im ((Stone-retraction (X,X0)),a) = (Stone-retraction (X,X0)) .: (MaxADSet a) let a be Point of X; ::_thesis: Im ((Stone-retraction (X,X0)),a) = (Stone-retraction (X,X0)) .: (MaxADSet a) set r = Stone-retraction (X,X0); A1: dom (Stone-retraction (X,X0)) = [#] X by FUNCT_2:def_1; A2: (Stone-retraction (X,X0)) .: ((Stone-retraction (X,X0)) " {((Stone-retraction (X,X0)) . a)}) c= {((Stone-retraction (X,X0)) . a)} by FUNCT_1:75; A3: (Stone-retraction (X,X0)) " {((Stone-retraction (X,X0)) . a)} = MaxADSet a by Th27; then (Stone-retraction (X,X0)) .: ((Stone-retraction (X,X0)) " {((Stone-retraction (X,X0)) . a)}) <> {} by A1, RELAT_1:119; then (Stone-retraction (X,X0)) .: ((Stone-retraction (X,X0)) " {((Stone-retraction (X,X0)) . a)}) = {((Stone-retraction (X,X0)) . a)} by A2, ZFMISC_1:33; hence Im ((Stone-retraction (X,X0)),a) = (Stone-retraction (X,X0)) .: (MaxADSet a) by A1, A3, FUNCT_1:59; ::_thesis: verum end; definition let X be non empty TopSpace; let X0 be non empty maximal_Kolmogorov_subspace of X; redefine func Stone-retraction (X,X0) means :Def12: :: TSP_2:def 12 for M being Subset of X st M = the carrier of X0 holds for A being Subset of X holds M /\ (MaxADSet A) = it .: A; compatibility for b1 being continuous Function of X,X0 holds ( b1 = Stone-retraction (X,X0) iff for M being Subset of X st M = the carrier of X0 holds for A being Subset of X holds M /\ (MaxADSet A) = b1 .: A ) proof let r be continuous Function of X,X0; ::_thesis: ( r = Stone-retraction (X,X0) iff for M being Subset of X st M = the carrier of X0 holds for A being Subset of X holds M /\ (MaxADSet A) = r .: A ) thus ( r = Stone-retraction (X,X0) implies for M being Subset of X st M = the carrier of X0 holds for A being Subset of X holds M /\ (MaxADSet A) = r .: A ) ::_thesis: ( ( for M being Subset of X st M = the carrier of X0 holds for A being Subset of X holds M /\ (MaxADSet A) = r .: A ) implies r = Stone-retraction (X,X0) ) proof assume A1: r = Stone-retraction (X,X0) ; ::_thesis: for M being Subset of X st M = the carrier of X0 holds for A being Subset of X holds M /\ (MaxADSet A) = r .: A let M be Subset of X; ::_thesis: ( M = the carrier of X0 implies for A being Subset of X holds M /\ (MaxADSet A) = r .: A ) reconsider N = M as Subset of X ; assume A2: M = the carrier of X0 ; ::_thesis: for A being Subset of X holds M /\ (MaxADSet A) = r .: A let A be Subset of X; ::_thesis: M /\ (MaxADSet A) = r .: A N is maximal_T_0 by A2, Th11; then A3: N is T_0 by Def4; for x being set st x in M /\ (MaxADSet A) holds x in r .: A proof let x be set ; ::_thesis: ( x in M /\ (MaxADSet A) implies x in r .: A ) assume A4: x in M /\ (MaxADSet A) ; ::_thesis: x in r .: A then reconsider c = x as Point of X ; c in M by A4, XBOOLE_0:def_4; then A5: M /\ (MaxADSet c) = {c} by A3, Def2; c in MaxADSet A by A4, XBOOLE_0:def_4; then c in union { (MaxADSet a) where a is Point of X : a in A } by TEX_4:def_11; then consider D being set such that A6: c in D and A7: D in { (MaxADSet a) where a is Point of X : a in A } by TARSKI:def_4; consider a being Point of X such that A8: D = MaxADSet a and A9: a in A by A7; MaxADSet c = MaxADSet a by A6, A8, TEX_4:21; then {(r . a)} = {c} by A1, A2, A5, Def10; hence x in r .: A by A9, FUNCT_2:35, ZFMISC_1:3; ::_thesis: verum end; then A10: M /\ (MaxADSet A) c= r .: A by TARSKI:def_3; for x being set st x in r .: A holds x in M /\ (MaxADSet A) proof let x be set ; ::_thesis: ( x in r .: A implies x in M /\ (MaxADSet A) ) assume A11: x in r .: A ; ::_thesis: x in M /\ (MaxADSet A) then reconsider b = x as Point of X0 ; consider a being set such that A12: a in the carrier of X and A13: a in A and A14: b = r . a by A11, FUNCT_2:64; reconsider a = a as Point of X by A12; {a} c= A by A13, ZFMISC_1:31; then MaxADSet {a} c= MaxADSet A by TEX_4:31; then MaxADSet a c= MaxADSet A by TEX_4:28; then A15: M /\ (MaxADSet a) c= M /\ (MaxADSet A) by XBOOLE_1:26; M /\ (MaxADSet a) = {b} by A1, A2, A14, Def10; hence x in M /\ (MaxADSet A) by A15, ZFMISC_1:31; ::_thesis: verum end; then r .: A c= M /\ (MaxADSet A) by TARSKI:def_3; hence M /\ (MaxADSet A) = r .: A by A10, XBOOLE_0:def_10; ::_thesis: verum end; assume A16: for M being Subset of X st M = the carrier of X0 holds for A being Subset of X holds M /\ (MaxADSet A) = r .: A ; ::_thesis: r = Stone-retraction (X,X0) A17: dom r = [#] X by FUNCT_2:def_1; for M being Subset of X st M = the carrier of X0 holds for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} proof let M be Subset of X; ::_thesis: ( M = the carrier of X0 implies for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) assume A18: M = the carrier of X0 ; ::_thesis: for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} let a be Point of X; ::_thesis: M /\ (MaxADSet a) = {(r . a)} M /\ (MaxADSet {a}) = Im (r,a) by A16, A18; then M /\ (MaxADSet a) = Im (r,a) by TEX_4:28; hence M /\ (MaxADSet a) = {(r . a)} by A17, FUNCT_1:59; ::_thesis: verum end; hence r = Stone-retraction (X,X0) by Def10; ::_thesis: verum end; end; :: deftheorem Def12 defines Stone-retraction TSP_2:def_12_:_ for X being non empty TopSpace for X0 being non empty maximal_Kolmogorov_subspace of X for b3 being continuous Function of X,X0 holds ( b3 = Stone-retraction (X,X0) iff for M being Subset of X st M = the carrier of X0 holds for A being Subset of X holds M /\ (MaxADSet A) = b3 .: A ); theorem Th29: :: TSP_2:29 for X being non empty TopSpace for X0 being non empty maximal_Kolmogorov_subspace of X for A being Subset of X holds (Stone-retraction (X,X0)) " ((Stone-retraction (X,X0)) .: A) = MaxADSet A proof let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X for A being Subset of X holds (Stone-retraction (X,X0)) " ((Stone-retraction (X,X0)) .: A) = MaxADSet A let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for A being Subset of X holds (Stone-retraction (X,X0)) " ((Stone-retraction (X,X0)) .: A) = MaxADSet A let A be Subset of X; ::_thesis: (Stone-retraction (X,X0)) " ((Stone-retraction (X,X0)) .: A) = MaxADSet A reconsider C = the carrier of X0 as non empty Subset of X by TSEP_1:1; set r = Stone-retraction (X,X0); C c= the carrier of X ; then reconsider B = (Stone-retraction (X,X0)) .: A as Subset of X by XBOOLE_1:1; C /\ (MaxADSet A) = B by Def12; then A1: B c= MaxADSet A by XBOOLE_1:17; A2: (Stone-retraction (X,X0)) " ((Stone-retraction (X,X0)) .: A) = MaxADSet B by Th26; then A c= MaxADSet B by FUNCT_2:42; hence (Stone-retraction (X,X0)) " ((Stone-retraction (X,X0)) .: A) = MaxADSet A by A2, A1, TEX_4:35; ::_thesis: verum end; theorem :: TSP_2:30 for X being non empty TopSpace for X0 being non empty maximal_Kolmogorov_subspace of X for A being Subset of X holds (Stone-retraction (X,X0)) .: A = (Stone-retraction (X,X0)) .: (MaxADSet A) proof let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X for A being Subset of X holds (Stone-retraction (X,X0)) .: A = (Stone-retraction (X,X0)) .: (MaxADSet A) let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for A being Subset of X holds (Stone-retraction (X,X0)) .: A = (Stone-retraction (X,X0)) .: (MaxADSet A) let A be Subset of X; ::_thesis: (Stone-retraction (X,X0)) .: A = (Stone-retraction (X,X0)) .: (MaxADSet A) set r = Stone-retraction (X,X0); A1: rng (Stone-retraction (X,X0)) = (Stone-retraction (X,X0)) .: the carrier of X by RELSET_1:22; (Stone-retraction (X,X0)) .: ((Stone-retraction (X,X0)) " ((Stone-retraction (X,X0)) .: A)) = (Stone-retraction (X,X0)) .: (MaxADSet A) by Th29; hence (Stone-retraction (X,X0)) .: A = (Stone-retraction (X,X0)) .: (MaxADSet A) by A1, FUNCT_1:77, RELAT_1:123; ::_thesis: verum end; theorem :: TSP_2:31 for X being non empty TopSpace for X0 being non empty maximal_Kolmogorov_subspace of X for A, B being Subset of X holds (Stone-retraction (X,X0)) .: (A \/ B) = ((Stone-retraction (X,X0)) .: A) \/ ((Stone-retraction (X,X0)) .: B) proof let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X for A, B being Subset of X holds (Stone-retraction (X,X0)) .: (A \/ B) = ((Stone-retraction (X,X0)) .: A) \/ ((Stone-retraction (X,X0)) .: B) let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for A, B being Subset of X holds (Stone-retraction (X,X0)) .: (A \/ B) = ((Stone-retraction (X,X0)) .: A) \/ ((Stone-retraction (X,X0)) .: B) reconsider M = the carrier of X0 as Subset of X by TSEP_1:1; set r = Stone-retraction (X,X0); let A, B be Subset of X; ::_thesis: (Stone-retraction (X,X0)) .: (A \/ B) = ((Stone-retraction (X,X0)) .: A) \/ ((Stone-retraction (X,X0)) .: B) (Stone-retraction (X,X0)) .: (A \/ B) = M /\ (MaxADSet (A \/ B)) by Def12 .= M /\ ((MaxADSet A) \/ (MaxADSet B)) by TEX_4:36 .= (M /\ (MaxADSet A)) \/ (M /\ (MaxADSet B)) by XBOOLE_1:23 .= ((Stone-retraction (X,X0)) .: A) \/ (M /\ (MaxADSet B)) by Def12 .= ((Stone-retraction (X,X0)) .: A) \/ ((Stone-retraction (X,X0)) .: B) by Def12 ; hence (Stone-retraction (X,X0)) .: (A \/ B) = ((Stone-retraction (X,X0)) .: A) \/ ((Stone-retraction (X,X0)) .: B) ; ::_thesis: verum end; theorem :: TSP_2:32 for X being non empty TopSpace for X0 being non empty maximal_Kolmogorov_subspace of X for A, B being Subset of X st ( A is open or B is open ) holds (Stone-retraction (X,X0)) .: (A /\ B) = ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B) proof let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X for A, B being Subset of X st ( A is open or B is open ) holds (Stone-retraction (X,X0)) .: (A /\ B) = ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B) let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for A, B being Subset of X st ( A is open or B is open ) holds (Stone-retraction (X,X0)) .: (A /\ B) = ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B) reconsider M = the carrier of X0 as Subset of X by TSEP_1:1; set r = Stone-retraction (X,X0); let A, B be Subset of X; ::_thesis: ( ( A is open or B is open ) implies (Stone-retraction (X,X0)) .: (A /\ B) = ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B) ) assume A1: ( A is open or B is open ) ; ::_thesis: (Stone-retraction (X,X0)) .: (A /\ B) = ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B) (Stone-retraction (X,X0)) .: (A /\ B) = M /\ (MaxADSet (A /\ B)) by Def12 .= (M /\ M) /\ ((MaxADSet A) /\ (MaxADSet B)) by A1, TEX_4:65 .= M /\ (M /\ ((MaxADSet A) /\ (MaxADSet B))) by XBOOLE_1:16 .= ((M /\ (MaxADSet A)) /\ (MaxADSet B)) /\ M by XBOOLE_1:16 .= (M /\ (MaxADSet A)) /\ (M /\ (MaxADSet B)) by XBOOLE_1:16 .= ((Stone-retraction (X,X0)) .: A) /\ (M /\ (MaxADSet B)) by Def12 .= ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B) by Def12 ; hence (Stone-retraction (X,X0)) .: (A /\ B) = ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B) ; ::_thesis: verum end; theorem :: TSP_2:33 for X being non empty TopSpace for X0 being non empty maximal_Kolmogorov_subspace of X for A, B being Subset of X st ( A is closed or B is closed ) holds (Stone-retraction (X,X0)) .: (A /\ B) = ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B) proof let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X for A, B being Subset of X st ( A is closed or B is closed ) holds (Stone-retraction (X,X0)) .: (A /\ B) = ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B) let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for A, B being Subset of X st ( A is closed or B is closed ) holds (Stone-retraction (X,X0)) .: (A /\ B) = ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B) reconsider M = the carrier of X0 as Subset of X by TSEP_1:1; set r = Stone-retraction (X,X0); let A, B be Subset of X; ::_thesis: ( ( A is closed or B is closed ) implies (Stone-retraction (X,X0)) .: (A /\ B) = ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B) ) assume A1: ( A is closed or B is closed ) ; ::_thesis: (Stone-retraction (X,X0)) .: (A /\ B) = ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B) (Stone-retraction (X,X0)) .: (A /\ B) = M /\ (MaxADSet (A /\ B)) by Def12 .= (M /\ M) /\ ((MaxADSet A) /\ (MaxADSet B)) by A1, TEX_4:64 .= M /\ (M /\ ((MaxADSet A) /\ (MaxADSet B))) by XBOOLE_1:16 .= ((M /\ (MaxADSet A)) /\ (MaxADSet B)) /\ M by XBOOLE_1:16 .= (M /\ (MaxADSet A)) /\ (M /\ (MaxADSet B)) by XBOOLE_1:16 .= ((Stone-retraction (X,X0)) .: A) /\ (M /\ (MaxADSet B)) by Def12 .= ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B) by Def12 ; hence (Stone-retraction (X,X0)) .: (A /\ B) = ((Stone-retraction (X,X0)) .: A) /\ ((Stone-retraction (X,X0)) .: B) ; ::_thesis: verum end; theorem :: TSP_2:34 for X being non empty TopSpace for X0 being non empty maximal_Kolmogorov_subspace of X for A being Subset of X st A is open holds (Stone-retraction (X,X0)) .: A is open proof let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X for A being Subset of X st A is open holds (Stone-retraction (X,X0)) .: A is open let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for A being Subset of X st A is open holds (Stone-retraction (X,X0)) .: A is open let A be Subset of X; ::_thesis: ( A is open implies (Stone-retraction (X,X0)) .: A is open ) reconsider M = the carrier of X0 as Subset of X by TSEP_1:1; set B = (Stone-retraction (X,X0)) .: A; assume A1: A is open ; ::_thesis: (Stone-retraction (X,X0)) .: A is open then A = MaxADSet A by TEX_4:56; then A /\ M = (Stone-retraction (X,X0)) .: A by Def12; hence (Stone-retraction (X,X0)) .: A is open by A1, TSP_1:def_1; ::_thesis: verum end; theorem :: TSP_2:35 for X being non empty TopSpace for X0 being non empty maximal_Kolmogorov_subspace of X for A being Subset of X st A is closed holds (Stone-retraction (X,X0)) .: A is closed proof let X be non empty TopSpace; ::_thesis: for X0 being non empty maximal_Kolmogorov_subspace of X for A being Subset of X st A is closed holds (Stone-retraction (X,X0)) .: A is closed let X0 be non empty maximal_Kolmogorov_subspace of X; ::_thesis: for A being Subset of X st A is closed holds (Stone-retraction (X,X0)) .: A is closed let A be Subset of X; ::_thesis: ( A is closed implies (Stone-retraction (X,X0)) .: A is closed ) reconsider M = the carrier of X0 as Subset of X by TSEP_1:1; set B = (Stone-retraction (X,X0)) .: A; assume A1: A is closed ; ::_thesis: (Stone-retraction (X,X0)) .: A is closed then A = MaxADSet A by TEX_4:60; then A /\ M = (Stone-retraction (X,X0)) .: A by Def12; hence (Stone-retraction (X,X0)) .: A is closed by A1, TSP_1:def_2; ::_thesis: verum end;