:: TEX_3 semantic presentation

begin


theorem Th1: :: TEX_3:1
for X being non empty TopSpace
for A, B being Subset of X st A,B constitute_a_decomposition holds
( not A is empty iff B is proper )
proof
let X be non empty TopSpace; ::_thesis: for A, B being Subset of X st A,B constitute_a_decomposition holds
( not A is empty iff B is proper )
let A, B be Subset of X; ::_thesis: ( A,B constitute_a_decomposition implies ( not A is empty iff B is proper ) )
assume A1: A,B constitute_a_decomposition ; ::_thesis: ( not A is empty iff B is proper )
then A2: B = A ` by TSEP_2:3;
thus  ( not A is empty implies B is proper ) ::_thesis: ( B is proper implies not A is empty )
proof
assume  not A is empty ; ::_thesis: B is proper
then  B <> the carrier of X by A2, TOPS_3:1;
hence  B is proper by SUBSET_1:def_6; ::_thesis: verum
end;
assume A3: B is proper ; ::_thesis: not A is empty
 A = B ` by A1, TSEP_2:3;
hence  not A is empty by A3; ::_thesis: verum
end;

Lm1:  for X being non empty TopSpace
for A, B being Subset of X st A is everywhere_dense & B is everywhere_dense holds
A meets B
proof
let X be non empty TopSpace; ::_thesis: for A, B being Subset of X st A is everywhere_dense & B is everywhere_dense holds
A meets B
let A, B be Subset of X; ::_thesis: ( A is everywhere_dense & B is everywhere_dense implies A meets B )
assume  ( A is everywhere_dense & B is everywhere_dense ) ; ::_thesis: A meets B
then  A /\ B <> {} by TOPS_3:34, TOPS_3:44;
hence  A meets B by XBOOLE_0:def_7; ::_thesis: verum
end;

Lm2:  for X being non empty TopSpace
for A, B being Subset of X st ( ( A is everywhere_dense & B is dense ) or ( A is dense & B is everywhere_dense ) ) holds
A meets B
proof
let X be non empty TopSpace; ::_thesis: for A, B being Subset of X st ( ( A is everywhere_dense & B is dense ) or ( A is dense & B is everywhere_dense ) ) holds
A meets B
let A, B be Subset of X; ::_thesis: ( ( ( A is everywhere_dense & B is dense ) or ( A is dense & B is everywhere_dense ) ) implies A meets B )
assume  ( ( A is everywhere_dense & B is dense ) or ( A is dense & B is everywhere_dense ) ) ; ::_thesis: A meets B
then  A /\ B <> {} by TOPS_3:17, TOPS_3:45;
hence  A meets B by XBOOLE_0:def_7; ::_thesis: verum
end;

theorem Th2: :: TEX_3:2
for X being non empty TopSpace
for A, B being Subset of X st A,B constitute_a_decomposition holds
( A is dense iff B is boundary )
proof
let X be non empty TopSpace; ::_thesis: for A, B being Subset of X st A,B constitute_a_decomposition holds
( A is dense iff B is boundary )
let A, B be Subset of X; ::_thesis: ( A,B constitute_a_decomposition implies ( A is dense iff B is boundary ) )
assume A1: A,B constitute_a_decomposition ; ::_thesis: ( A is dense iff B is boundary )
then  B = A ` by TSEP_2:3;
hence  ( A is dense implies B is boundary ) by TOPS_3:18; ::_thesis: ( B is boundary implies A is dense )
assume A2: B is boundary ; ::_thesis: A is dense
 A = B ` by A1, TSEP_2:3;
hence  A is dense by A2, TOPS_1:def_4; ::_thesis: verum
end;

theorem :: TEX_3:3
for X being non empty TopSpace
for A, B being Subset of X st A,B constitute_a_decomposition holds
( A is boundary iff B is dense ) by Th2;

theorem Th4: :: TEX_3:4
for X being non empty TopSpace
for A, B being Subset of X st A,B constitute_a_decomposition holds
( A is everywhere_dense iff B is nowhere_dense )
proof
let X be non empty TopSpace; ::_thesis: for A, B being Subset of X st A,B constitute_a_decomposition holds
( A is everywhere_dense iff B is nowhere_dense )
let A, B be Subset of X; ::_thesis: ( A,B constitute_a_decomposition implies ( A is everywhere_dense iff B is nowhere_dense ) )
assume A1: A,B constitute_a_decomposition ; ::_thesis: ( A is everywhere_dense iff B is nowhere_dense )
then  B = A ` by TSEP_2:3;
hence  ( A is everywhere_dense implies B is nowhere_dense ) by TOPS_3:39; ::_thesis: ( B is nowhere_dense implies A is everywhere_dense )
assume A2: B is nowhere_dense ; ::_thesis: A is everywhere_dense
 A = B ` by A1, TSEP_2:3;
hence  A is everywhere_dense by A2, TOPS_3:40; ::_thesis: verum
end;

theorem :: TEX_3:5
for X being non empty TopSpace
for A, B being Subset of X st A,B constitute_a_decomposition holds
( A is nowhere_dense iff B is everywhere_dense ) by Th4;


theorem Th6: :: TEX_3:6
for X being non empty TopSpace
for Y1, Y2 being non empty SubSpace of X st Y1,Y2 constitute_a_decomposition holds
( Y1 is proper & Y2 is proper )
proof
let X be non empty TopSpace; ::_thesis: for Y1, Y2 being non empty SubSpace of X st Y1,Y2 constitute_a_decomposition holds
( Y1 is proper & Y2 is proper )
let Y1, Y2 be non empty SubSpace of X; ::_thesis: ( Y1,Y2 constitute_a_decomposition implies ( Y1 is proper & Y2 is proper ) )
reconsider A1 = the carrier of Y1, A2 = the carrier of Y2 as Subset of X by TSEP_1:1;
assume  Y1,Y2 constitute_a_decomposition ; ::_thesis: ( Y1 is proper & Y2 is proper )
then  A1,A2 constitute_a_decomposition by TSEP_2:def_2;
then  ( A1 is proper & A2 is proper ) by Th1;
hence  ( Y1 is proper & Y2 is proper ) by TEX_2:8; ::_thesis: verum
end;

theorem :: TEX_3:7
for X being non trivial TopSpace
for D being non empty proper Subset of X ex Y0 being non empty strict proper SubSpace of X st D = the carrier of Y0
proof
let X be non trivial TopSpace; ::_thesis: for D being non empty proper Subset of X ex Y0 being non empty strict proper SubSpace of X st D = the carrier of Y0
let D be non empty proper Subset of X; ::_thesis: ex Y0 being non empty strict proper SubSpace of X st D = the carrier of Y0
consider Y0 being non empty strict SubSpace of X such that
A1: D = the carrier of Y0 by TSEP_1:10;
reconsider Y0 = Y0 as non empty strict proper SubSpace of X by A1, TEX_2:8;
take  Y0 ; ::_thesis: D = the carrier of Y0
thus  D = the carrier of Y0 by A1; ::_thesis: verum
end;

theorem Th8: :: TEX_3:8
for X being non trivial TopSpace
for Y1 being non empty proper SubSpace of X ex Y2 being non empty strict proper SubSpace of X st Y1,Y2 constitute_a_decomposition
proof
let X be non trivial TopSpace; ::_thesis: for Y1 being non empty proper SubSpace of X ex Y2 being non empty strict proper SubSpace of X st Y1,Y2 constitute_a_decomposition
let Y1 be non empty proper SubSpace of X; ::_thesis: ex Y2 being non empty strict proper SubSpace of X st Y1,Y2 constitute_a_decomposition
reconsider A1 = the carrier of Y1 as Subset of X by TSEP_1:1;
 A1 is proper by TEX_2:8;
then consider Y2 being non empty strict SubSpace of X such that
A1: A1 ` = the carrier of Y2 by TSEP_1:10;
A2: for P, Q being Subset of X st P = the carrier of Y1 & Q = the carrier of Y2 holds
P,Q constitute_a_decomposition by A1, TSEP_2:5;
then  Y1,Y2 constitute_a_decomposition by TSEP_2:def_2;
then reconsider Y2 = Y2 as non empty strict proper SubSpace of X by Th6;
take  Y2 ; ::_thesis: Y1,Y2 constitute_a_decomposition
thus  Y1,Y2 constitute_a_decomposition by A2, TSEP_2:def_2; ::_thesis: verum
end;

begin

definition
let X be non empty TopSpace;
let IT be SubSpace of X;
attrIT is dense  means :Def1: :: TEX_3:def 1
 for A being Subset of X st A = the carrier of IT holds
A is dense ;
end;

:: deftheorem Def1 defines dense TEX_3:def_1_:_
 for X being non empty TopSpace
for IT being SubSpace of X holds
( IT is dense iff for A being Subset of X st A = the carrier of IT holds
A is dense );

theorem Th9: :: TEX_3:9
for X being non empty TopSpace
for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is dense iff A is dense )
proof
let X be non empty TopSpace; ::_thesis: for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is dense iff A is dense )
let X0 be SubSpace of X; ::_thesis: for A being Subset of X st A = the carrier of X0 holds
( X0 is dense iff A is dense )
let A be Subset of X; ::_thesis: ( A = the carrier of X0 implies ( X0 is dense iff A is dense ) )
assume A1: A = the carrier of X0 ; ::_thesis: ( X0 is dense iff A is dense )
hence  ( X0 is dense implies A is dense ) by Def1; ::_thesis: ( A is dense implies X0 is dense )
assume  A is dense ; ::_thesis: X0 is dense
then  for B being Subset of X st B = the carrier of X0 holds
B is dense by A1;
hence  X0 is dense by Def1; ::_thesis: verum
end;

registration
let X be non empty TopSpace;
cluster closed dense  ->  non proper for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is dense & b1 is closed holds
not b1 is proper
proof
let X0 be SubSpace of X; ::_thesis: ( X0 is dense & X0 is closed implies not X0 is proper )
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
assume A1: ( X0 is dense & X0 is closed ) ; ::_thesis: not X0 is proper
then  A is closed by TSEP_1:11;
then A2: Cl A = A by PRE_TOPC:22;
 A is dense by A1, Th9;
then  Cl A = the carrier of X by TOPS_3:def_2;
then  not A is proper by A2, SUBSET_1:def_6;
hence  not X0 is proper by TEX_2:8; ::_thesis: verum
end;
cluster proper dense  ->  non closed for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is dense & b1 is proper holds
not b1 is closed ;
cluster closed proper  ->  non dense for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is proper & b1 is closed holds
not b1 is dense ;
end;

registration
let X be non empty TopSpace;
cluster non empty strict TopSpace-like dense for SubSpace of X;
existence
 ex b1 being SubSpace of X st
( b1 is dense & b1 is strict & not b1 is empty )
proof
 X is SubSpace of X by TSEP_1:2;
then reconsider A0 = the carrier of X as Subset of X by TSEP_1:1;
consider X0 being non empty strict SubSpace of X such that
A1: A0 = the carrier of X0 by TSEP_1:10;
take  X0 ; ::_thesis: ( X0 is dense & X0 is strict & not X0 is empty )
now__::_thesis:_for_A_being_Subset_of_X_st_A_=_the_carrier_of_X0_holds_
A_is_dense
let A be Subset of X; ::_thesis: ( A = the carrier of X0 implies A is dense )
assume  A = the carrier of X0 ; ::_thesis: A is dense
then  A = [#] X by A1;
hence  A is dense ; ::_thesis: verum
end;
hence  ( X0 is dense & X0 is strict & not X0 is empty ) by Def1; ::_thesis: verum
end;
end;

theorem Th10: :: TEX_3:10
for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is dense holds
ex X0 being non empty strict dense SubSpace of X st A0 = the carrier of X0
proof
let X be non empty TopSpace; ::_thesis: for A0 being non empty Subset of X st A0 is dense holds
ex X0 being non empty strict dense SubSpace of X st A0 = the carrier of X0
let A0 be non empty Subset of X; ::_thesis: ( A0 is dense implies ex X0 being non empty strict dense SubSpace of X st A0 = the carrier of X0 )
consider X0 being non empty strict SubSpace of X such that
A1: A0 = the carrier of X0 by TSEP_1:10;
assume  A0 is dense ; ::_thesis: ex X0 being non empty strict dense SubSpace of X st A0 = the carrier of X0
then reconsider Y0 = X0 as non empty strict dense SubSpace of X by A1, Th9;
take  Y0 ; ::_thesis: A0 = the carrier of Y0
thus  A0 = the carrier of Y0 by A1; ::_thesis: verum
end;

theorem :: TEX_3:11
for X being non empty TopSpace
for X0 being non empty dense SubSpace of X
for A being Subset of X
for B being Subset of X0 st A = B holds
( B is dense iff A is dense )
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty dense SubSpace of X
for A being Subset of X
for B being Subset of X0 st A = B holds
( B is dense iff A is dense )
let X0 be non empty dense SubSpace of X; ::_thesis: for A being Subset of X
for B being Subset of X0 st A = B holds
( B is dense iff A is dense )
let A be Subset of X; ::_thesis: for B being Subset of X0 st A = B holds
( B is dense iff A is dense )
let B be Subset of X0; ::_thesis: ( A = B implies ( B is dense iff A is dense ) )
assume A1: A = B ; ::_thesis: ( B is dense iff A is dense )
reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
 C is dense by Th9;
hence  ( B is dense iff A is dense ) by A1, TOPS_3:60; ::_thesis: verum
end;

theorem :: TEX_3:12
for X being non empty TopSpace
for X1 being dense SubSpace of X
for X2 being SubSpace of X st X1 is SubSpace of X2 holds
X2 is dense
proof
let X be non empty TopSpace; ::_thesis: for X1 being dense SubSpace of X
for X2 being SubSpace of X st X1 is SubSpace of X2 holds
X2 is dense
let X1 be dense SubSpace of X; ::_thesis: for X2 being SubSpace of X st X1 is SubSpace of X2 holds
X2 is dense
let X2 be SubSpace of X; ::_thesis: ( X1 is SubSpace of X2 implies X2 is dense )
reconsider C = the carrier of X1 as Subset of X by BORSUK_1:1;
assume  X1 is SubSpace of X2 ; ::_thesis: X2 is dense
then A1: the carrier of X1 c= the carrier of X2 by TSEP_1:4;
 C is dense by Def1;
then  for A being Subset of X st A = the carrier of X2 holds
A is dense by A1, TOPS_1:44;
hence  X2 is dense by Def1; ::_thesis: verum
end;

theorem :: TEX_3:13
for X being non empty TopSpace
for X1 being non empty dense SubSpace of X
for X2 being non empty SubSpace of X st X1 is SubSpace of X2 holds
X1 is dense SubSpace of X2
proof
let X be non empty TopSpace; ::_thesis: for X1 being non empty dense SubSpace of X
for X2 being non empty SubSpace of X st X1 is SubSpace of X2 holds
X1 is dense SubSpace of X2
let X1 be non empty dense SubSpace of X; ::_thesis: for X2 being non empty SubSpace of X st X1 is SubSpace of X2 holds
X1 is dense SubSpace of X2
let X2 be non empty SubSpace of X; ::_thesis: ( X1 is SubSpace of X2 implies X1 is dense SubSpace of X2 )
reconsider C = the carrier of X1 as Subset of X by BORSUK_1:1;
 C is dense by Def1;
then A1: for A being Subset of X2 st A = the carrier of X1 holds
A is dense by TOPS_3:59;
assume  X1 is SubSpace of X2 ; ::_thesis: X1 is dense SubSpace of X2
hence  X1 is dense SubSpace of X2 by A1, Def1; ::_thesis: verum
end;

theorem :: TEX_3:14
for X being non empty TopSpace
for X1 being non empty dense SubSpace of X
for X2 being non empty dense SubSpace of X1 holds X2 is non empty dense SubSpace of X
proof
let X be non empty TopSpace; ::_thesis: for X1 being non empty dense SubSpace of X
for X2 being non empty dense SubSpace of X1 holds X2 is non empty dense SubSpace of X
let X1 be non empty dense SubSpace of X; ::_thesis: for X2 being non empty dense SubSpace of X1 holds X2 is non empty dense SubSpace of X
let X2 be non empty dense SubSpace of X1; ::_thesis: X2 is non empty dense SubSpace of X
reconsider C = the carrier of X1 as Subset of X by BORSUK_1:1;
now__::_thesis:_for_A_being_Subset_of_X_st_A_=_the_carrier_of_X2_holds_
A_is_dense
let A be Subset of X; ::_thesis: ( A = the carrier of X2 implies A is dense )
assume A1: A = the carrier of X2 ; ::_thesis: A is dense
then reconsider B = A as Subset of X1 by BORSUK_1:1;
A2: C is dense by Def1;
 B is dense by A1, Def1;
hence  A is dense by A2, TOPS_3:60; ::_thesis: verum
end;
hence  X2 is non empty dense SubSpace of X by Def1, TSEP_1:7; ::_thesis: verum
end;

theorem :: TEX_3:15
for X, Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1, the topology of Y1 #) holds
( Y1 is dense SubSpace of X iff Y2 is dense SubSpace of X )
proof
let X be non empty TopSpace; ::_thesis: for Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1, the topology of Y1 #) holds
( Y1 is dense SubSpace of X iff Y2 is dense SubSpace of X )
let X1, X2 be non empty TopSpace; ::_thesis: ( X2 = TopStruct(# the carrier of X1, the topology of X1 #) implies ( X1 is dense SubSpace of X iff X2 is dense SubSpace of X ) )
assume A1: X2 = TopStruct(# the carrier of X1, the topology of X1 #) ; ::_thesis: ( X1 is dense SubSpace of X iff X2 is dense SubSpace of X )
thus  ( X1 is dense SubSpace of X implies X2 is dense SubSpace of X ) ::_thesis: ( X2 is dense SubSpace of X implies X1 is dense SubSpace of X )
proof
assume A2: X1 is dense SubSpace of X ; ::_thesis: X2 is dense SubSpace of X
then reconsider Y2 = X2 as SubSpace of X by A1, TMAP_1:7;
 for A2 being Subset of X st A2 = the carrier of Y2 holds
A2 is dense by A1, A2, Def1;
hence  X2 is dense SubSpace of X by Def1; ::_thesis: verum
end;
assume A3: X2 is dense SubSpace of X ; ::_thesis: X1 is dense SubSpace of X
then reconsider Y1 = X1 as SubSpace of X by A1, TMAP_1:7;
 for A1 being Subset of X st A1 = the carrier of Y1 holds
A1 is dense by A1, A3, Def1;
hence  X1 is dense SubSpace of X by Def1; ::_thesis: verum
end;

definition
let X be non empty TopSpace;
let IT be SubSpace of X;
attrIT is everywhere_dense  means :Def2: :: TEX_3:def 2
 for A being Subset of X st A = the carrier of IT holds
A is everywhere_dense ;
end;

:: deftheorem Def2 defines everywhere_dense TEX_3:def_2_:_
 for X being non empty TopSpace
for IT being SubSpace of X holds
( IT is everywhere_dense iff for A being Subset of X st A = the carrier of IT holds
A is everywhere_dense );

theorem Th16: :: TEX_3:16
for X being non empty TopSpace
for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is everywhere_dense iff A is everywhere_dense )
proof
let X be non empty TopSpace; ::_thesis: for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is everywhere_dense iff A is everywhere_dense )
let X0 be SubSpace of X; ::_thesis: for A being Subset of X st A = the carrier of X0 holds
( X0 is everywhere_dense iff A is everywhere_dense )
let A be Subset of X; ::_thesis: ( A = the carrier of X0 implies ( X0 is everywhere_dense iff A is everywhere_dense ) )
assume A1: A = the carrier of X0 ; ::_thesis: ( X0 is everywhere_dense iff A is everywhere_dense )
hence  ( X0 is everywhere_dense implies A is everywhere_dense ) by Def2; ::_thesis: ( A is everywhere_dense implies X0 is everywhere_dense )
assume  A is everywhere_dense ; ::_thesis: X0 is everywhere_dense
then  for B being Subset of X st B = the carrier of X0 holds
B is everywhere_dense by A1;
hence  X0 is everywhere_dense by Def2; ::_thesis: verum
end;

registration
let X be non empty TopSpace;
cluster everywhere_dense  ->  dense for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is everywhere_dense holds
b1 is dense
proof
let X0 be SubSpace of X; ::_thesis: ( X0 is everywhere_dense implies X0 is dense )
assume A1: X0 is everywhere_dense ; ::_thesis: X0 is dense
now__::_thesis:_for_A_being_Subset_of_X_st_A_=_the_carrier_of_X0_holds_
A_is_dense
let A be Subset of X; ::_thesis: ( A = the carrier of X0 implies A is dense )
assume  A = the carrier of X0 ; ::_thesis: A is dense
then  A is everywhere_dense by A1, Def2;
hence  A is dense by TOPS_3:33; ::_thesis: verum
end;
hence  X0 is dense by Def1; ::_thesis: verum
end;
cluster non dense  ->  non everywhere_dense for SubSpace of X;
coherence
 for b1 being SubSpace of X st not b1 is dense holds
not b1 is everywhere_dense ;
cluster non proper  ->  everywhere_dense for SubSpace of X;
coherence
 for b1 being SubSpace of X st not b1 is proper holds
b1 is everywhere_dense
proof
let X0 be SubSpace of X; ::_thesis: ( not X0 is proper implies X0 is everywhere_dense )
assume A2: not X0 is proper ; ::_thesis: X0 is everywhere_dense
now__::_thesis:_for_A_being_Subset_of_X_st_A_=_the_carrier_of_X0_holds_
A_is_everywhere_dense
let A be Subset of X; ::_thesis: ( A = the carrier of X0 implies A is everywhere_dense )
assume  A = the carrier of X0 ; ::_thesis: A is everywhere_dense
then  not A is proper by A2, TEX_2:8;
then  A = [#] X by SUBSET_1:def_6;
hence  A is everywhere_dense by TOPS_3:31; ::_thesis: verum
end;
hence  X0 is everywhere_dense by Def2; ::_thesis: verum
end;
cluster non everywhere_dense  ->  proper for SubSpace of X;
coherence
 for b1 being SubSpace of X st not b1 is everywhere_dense holds
b1 is proper ;
end;

registration
let X be non empty TopSpace;
cluster non empty strict TopSpace-like everywhere_dense for SubSpace of X;
existence
 ex b1 being SubSpace of X st
( b1 is everywhere_dense & b1 is strict & not b1 is empty )
proof
 X is SubSpace of X by TSEP_1:2;
then reconsider A0 = the carrier of X as Subset of X by TSEP_1:1;
consider X0 being non empty strict SubSpace of X such that
A1: A0 = the carrier of X0 by TSEP_1:10;
take  X0 ; ::_thesis: ( X0 is everywhere_dense & X0 is strict & not X0 is empty )
now__::_thesis:_for_A_being_Subset_of_X_st_A_=_the_carrier_of_X0_holds_
A_is_everywhere_dense
let A be Subset of X; ::_thesis: ( A = the carrier of X0 implies A is everywhere_dense )
assume  A = the carrier of X0 ; ::_thesis: A is everywhere_dense
then  A = [#] X by A1;
hence  A is everywhere_dense by TOPS_3:31; ::_thesis: verum
end;
hence  ( X0 is everywhere_dense & X0 is strict & not X0 is empty ) by Def2; ::_thesis: verum
end;
end;

theorem Th17: :: TEX_3:17
for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is everywhere_dense holds
ex X0 being non empty strict everywhere_dense SubSpace of X st A0 = the carrier of X0
proof
let X be non empty TopSpace; ::_thesis: for A0 being non empty Subset of X st A0 is everywhere_dense holds
ex X0 being non empty strict everywhere_dense SubSpace of X st A0 = the carrier of X0
let A0 be non empty Subset of X; ::_thesis: ( A0 is everywhere_dense implies ex X0 being non empty strict everywhere_dense SubSpace of X st A0 = the carrier of X0 )
consider X0 being non empty strict SubSpace of X such that
A1: A0 = the carrier of X0 by TSEP_1:10;
assume  A0 is everywhere_dense ; ::_thesis: ex X0 being non empty strict everywhere_dense SubSpace of X st A0 = the carrier of X0
then reconsider Y0 = X0 as non empty strict everywhere_dense SubSpace of X by A1, Th16;
take  Y0 ; ::_thesis: A0 = the carrier of Y0
thus  A0 = the carrier of Y0 by A1; ::_thesis: verum
end;

theorem :: TEX_3:18
for X being non empty TopSpace
for X0 being non empty everywhere_dense SubSpace of X
for A being Subset of X
for B being Subset of X0 st A = B holds
( B is everywhere_dense iff A is everywhere_dense )
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty everywhere_dense SubSpace of X
for A being Subset of X
for B being Subset of X0 st A = B holds
( B is everywhere_dense iff A is everywhere_dense )
let X0 be non empty everywhere_dense SubSpace of X; ::_thesis: for A being Subset of X
for B being Subset of X0 st A = B holds
( B is everywhere_dense iff A is everywhere_dense )
let A be Subset of X; ::_thesis: for B being Subset of X0 st A = B holds
( B is everywhere_dense iff A is everywhere_dense )
let B be Subset of X0; ::_thesis: ( A = B implies ( B is everywhere_dense iff A is everywhere_dense ) )
assume A1: A = B ; ::_thesis: ( B is everywhere_dense iff A is everywhere_dense )
reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
 C is everywhere_dense by Th16;
hence  ( B is everywhere_dense iff A is everywhere_dense ) by A1, TOPS_3:64; ::_thesis: verum
end;

theorem :: TEX_3:19
for X being non empty TopSpace
for X1 being everywhere_dense SubSpace of X
for X2 being SubSpace of X st X1 is SubSpace of X2 holds
X2 is everywhere_dense
proof
let X be non empty TopSpace; ::_thesis: for X1 being everywhere_dense SubSpace of X
for X2 being SubSpace of X st X1 is SubSpace of X2 holds
X2 is everywhere_dense
let X1 be everywhere_dense SubSpace of X; ::_thesis: for X2 being SubSpace of X st X1 is SubSpace of X2 holds
X2 is everywhere_dense
let X2 be SubSpace of X; ::_thesis: ( X1 is SubSpace of X2 implies X2 is everywhere_dense )
reconsider C = the carrier of X1 as Subset of X by BORSUK_1:1;
assume  X1 is SubSpace of X2 ; ::_thesis: X2 is everywhere_dense
then A1: the carrier of X1 c= the carrier of X2 by TSEP_1:4;
 C is everywhere_dense by Def2;
then  for A being Subset of X st A = the carrier of X2 holds
A is everywhere_dense by A1, TOPS_3:38;
hence  X2 is everywhere_dense by Def2; ::_thesis: verum
end;

theorem :: TEX_3:20
for X being non empty TopSpace
for X1 being non empty everywhere_dense SubSpace of X
for X2 being non empty SubSpace of X st X1 is SubSpace of X2 holds
X1 is everywhere_dense SubSpace of X2
proof
let X be non empty TopSpace; ::_thesis: for X1 being non empty everywhere_dense SubSpace of X
for X2 being non empty SubSpace of X st X1 is SubSpace of X2 holds
X1 is everywhere_dense SubSpace of X2
let X1 be non empty everywhere_dense SubSpace of X; ::_thesis: for X2 being non empty SubSpace of X st X1 is SubSpace of X2 holds
X1 is everywhere_dense SubSpace of X2
let X2 be non empty SubSpace of X; ::_thesis: ( X1 is SubSpace of X2 implies X1 is everywhere_dense SubSpace of X2 )
reconsider C = the carrier of X1 as Subset of X by BORSUK_1:1;
 C is everywhere_dense by Def2;
then A1: for A being Subset of X2 st A = the carrier of X1 holds
A is everywhere_dense by TOPS_3:61;
assume  X1 is SubSpace of X2 ; ::_thesis: X1 is everywhere_dense SubSpace of X2
hence  X1 is everywhere_dense SubSpace of X2 by A1, Def2; ::_thesis: verum
end;

theorem :: TEX_3:21
for X being non empty TopSpace
for X1 being non empty everywhere_dense SubSpace of X
for X2 being non empty everywhere_dense SubSpace of X1 holds X2 is everywhere_dense SubSpace of X
proof
let X be non empty TopSpace; ::_thesis: for X1 being non empty everywhere_dense SubSpace of X
for X2 being non empty everywhere_dense SubSpace of X1 holds X2 is everywhere_dense SubSpace of X
let X1 be non empty everywhere_dense SubSpace of X; ::_thesis: for X2 being non empty everywhere_dense SubSpace of X1 holds X2 is everywhere_dense SubSpace of X
let X2 be non empty everywhere_dense SubSpace of X1; ::_thesis: X2 is everywhere_dense SubSpace of X
reconsider C = the carrier of X1 as Subset of X by BORSUK_1:1;
now__::_thesis:_for_A_being_Subset_of_X_st_A_=_the_carrier_of_X2_holds_
A_is_everywhere_dense
let A be Subset of X; ::_thesis: ( A = the carrier of X2 implies A is everywhere_dense )
assume A1: A = the carrier of X2 ; ::_thesis: A is everywhere_dense
then reconsider B = A as Subset of X1 by BORSUK_1:1;
A2: C is everywhere_dense by Def2;
 B is everywhere_dense by A1, Def2;
hence  A is everywhere_dense by A2, TOPS_3:64; ::_thesis: verum
end;
hence  X2 is everywhere_dense SubSpace of X by Def2, TSEP_1:7; ::_thesis: verum
end;

theorem :: TEX_3:22
for X, Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1, the topology of Y1 #) holds
( Y1 is everywhere_dense SubSpace of X iff Y2 is everywhere_dense SubSpace of X )
proof
let X be non empty TopSpace; ::_thesis: for Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1, the topology of Y1 #) holds
( Y1 is everywhere_dense SubSpace of X iff Y2 is everywhere_dense SubSpace of X )
let X1, X2 be non empty TopSpace; ::_thesis: ( X2 = TopStruct(# the carrier of X1, the topology of X1 #) implies ( X1 is everywhere_dense SubSpace of X iff X2 is everywhere_dense SubSpace of X ) )
assume A1: X2 = TopStruct(# the carrier of X1, the topology of X1 #) ; ::_thesis: ( X1 is everywhere_dense SubSpace of X iff X2 is everywhere_dense SubSpace of X )
thus  ( X1 is everywhere_dense SubSpace of X implies X2 is everywhere_dense SubSpace of X ) ::_thesis: ( X2 is everywhere_dense SubSpace of X implies X1 is everywhere_dense SubSpace of X )
proof
assume A2: X1 is everywhere_dense SubSpace of X ; ::_thesis: X2 is everywhere_dense SubSpace of X
then reconsider Y2 = X2 as SubSpace of X by A1, TMAP_1:7;
 for A2 being Subset of X st A2 = the carrier of Y2 holds
A2 is everywhere_dense by A1, A2, Def2;
hence  X2 is everywhere_dense SubSpace of X by Def2; ::_thesis: verum
end;
assume A3: X2 is everywhere_dense SubSpace of X ; ::_thesis: X1 is everywhere_dense SubSpace of X
then reconsider Y1 = X1 as SubSpace of X by A1, TMAP_1:7;
 for A1 being Subset of X st A1 = the carrier of Y1 holds
A1 is everywhere_dense by A1, A3, Def2;
hence  X1 is everywhere_dense SubSpace of X by Def2; ::_thesis: verum
end;

registration
let X be non empty TopSpace;
cluster open dense  ->  everywhere_dense for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is dense & b1 is open holds
b1 is everywhere_dense
proof
let X0 be SubSpace of X; ::_thesis: ( X0 is dense & X0 is open implies X0 is everywhere_dense )
assume A1: ( X0 is dense & X0 is open ) ; ::_thesis: X0 is everywhere_dense
now__::_thesis:_for_A_being_Subset_of_X_st_A_=_the_carrier_of_X0_holds_
A_is_everywhere_dense
let A be Subset of X; ::_thesis: ( A = the carrier of X0 implies A is everywhere_dense )
assume  A = the carrier of X0 ; ::_thesis: A is everywhere_dense
then  ( A is dense & A is open ) by A1, Th9, TSEP_1:16;
hence  A is everywhere_dense by TOPS_3:36; ::_thesis: verum
end;
hence  X0 is everywhere_dense by Def2; ::_thesis: verum
end;
cluster dense non everywhere_dense  ->  non open for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is dense & not b1 is everywhere_dense holds
not b1 is open ;
cluster open non everywhere_dense  ->  non dense for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is open & not b1 is everywhere_dense holds
not b1 is dense ;
end;

registration
let X be non empty TopSpace;
cluster non empty strict TopSpace-like open dense for SubSpace of X;
existence
 ex b1 being SubSpace of X st
( b1 is dense & b1 is open & b1 is strict & not b1 is empty )
proof
 X is SubSpace of X by TSEP_1:2;
then reconsider A0 = the carrier of X as Subset of X by TSEP_1:1;
 A0 = [#] X ;
then  A0 is dense ;
then consider X0 being non empty strict dense SubSpace of X such that
A1: A0 = the carrier of X0 by Th10;
take  X0 ; ::_thesis: ( X0 is dense & X0 is open & X0 is strict & not X0 is empty )
now__::_thesis:_for_A_being_Subset_of_X_st_A_=_the_carrier_of_X0_holds_
A_is_open
let A be Subset of X; ::_thesis: ( A = the carrier of X0 implies A is open )
assume  A = the carrier of X0 ; ::_thesis: A is open
then  A = [#] X by A1;
hence  A is open ; ::_thesis: verum
end;
hence  ( X0 is dense & X0 is open & X0 is strict & not X0 is empty ) by TSEP_1:def_1; ::_thesis: verum
end;
end;

theorem Th23: :: TEX_3:23
for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is dense & A0 is open holds
ex X0 being non empty strict open dense SubSpace of X st A0 = the carrier of X0
proof
let X be non empty TopSpace; ::_thesis: for A0 being non empty Subset of X st A0 is dense & A0 is open holds
ex X0 being non empty strict open dense SubSpace of X st A0 = the carrier of X0
let A0 be non empty Subset of X; ::_thesis: ( A0 is dense & A0 is open implies ex X0 being non empty strict open dense SubSpace of X st A0 = the carrier of X0 )
consider X0 being non empty strict SubSpace of X such that
A1: A0 = the carrier of X0 by TSEP_1:10;
assume  ( A0 is dense & A0 is open ) ; ::_thesis: ex X0 being non empty strict open dense SubSpace of X st A0 = the carrier of X0
then reconsider Y0 = X0 as non empty strict open dense SubSpace of X by A1, Th9, TSEP_1:16;
take  Y0 ; ::_thesis: A0 = the carrier of Y0
thus  A0 = the carrier of Y0 by A1; ::_thesis: verum
end;

theorem :: TEX_3:24
for X being non empty TopSpace
for X0 being SubSpace of X holds
( X0 is everywhere_dense iff ex X1 being strict open dense SubSpace of X st X1 is SubSpace of X0 )
proof
let X be non empty TopSpace; ::_thesis: for X0 being SubSpace of X holds
( X0 is everywhere_dense iff ex X1 being strict open dense SubSpace of X st X1 is SubSpace of X0 )
let X0 be SubSpace of X; ::_thesis: ( X0 is everywhere_dense iff ex X1 being strict open dense SubSpace of X st X1 is SubSpace of X0 )
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
thus  ( X0 is everywhere_dense implies ex X1 being strict open dense SubSpace of X st X1 is SubSpace of X0 ) ::_thesis: ( ex X1 being strict open dense SubSpace of X st X1 is SubSpace of X0 implies X0 is everywhere_dense )
proof
assume  X0 is everywhere_dense ; ::_thesis: ex X1 being strict open dense SubSpace of X st X1 is SubSpace of X0
then  A is everywhere_dense by Def2;
then consider C being Subset of X such that
A1: C c= A and
A2: C is open and
A3: C is dense by TOPS_3:41;
 not C is empty by A3, TOPS_3:17;
then consider X1 being non empty strict open dense SubSpace of X such that
A4: C = the carrier of X1 by A2, A3, Th23;
take  X1 ; ::_thesis: X1 is SubSpace of X0
thus  X1 is SubSpace of X0 by A1, A4, TSEP_1:4; ::_thesis: verum
end;
given X1 being strict open dense SubSpace of X such that A5: X1 is SubSpace of X0 ; ::_thesis: X0 is everywhere_dense
reconsider C = the carrier of X1 as Subset of X by TSEP_1:1;
now__::_thesis:_ex_C_being_Subset_of_X_st_
(_C_c=_A_&_C_is_open_&_C_is_dense_)
take C = C; ::_thesis: ( C c= A & C is open & C is dense )
thus  ( C c= A & C is open & C is dense ) by A5, Def1, TSEP_1:4, TSEP_1:16; ::_thesis: verum
end;
then  for A being Subset of X st A = the carrier of X0 holds
A is everywhere_dense by TOPS_3:41;
hence  X0 is everywhere_dense by Def2; ::_thesis: verum
end;


theorem :: TEX_3:25
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st ( X1 is dense or X2 is dense ) holds
X1 union X2 is dense SubSpace of X
proof
let X be non empty TopSpace; ::_thesis: for X1, X2 being non empty SubSpace of X st ( X1 is dense or X2 is dense ) holds
X1 union X2 is dense SubSpace of X
let X1, X2 be non empty SubSpace of X; ::_thesis: ( ( X1 is dense or X2 is dense ) implies X1 union X2 is dense SubSpace of X )
reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
reconsider A = the carrier of (X1 union X2) as Subset of X by TSEP_1:1;
assume  ( X1 is dense or X2 is dense ) ; ::_thesis: X1 union X2 is dense SubSpace of X
then  ( A1 is dense or A2 is dense ) by Def1;
then  A1 \/ A2 is dense by TOPS_3:21;
then  A is dense by TSEP_1:def_2;
hence  X1 union X2 is dense SubSpace of X by Th9; ::_thesis: verum
end;

theorem :: TEX_3:26
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st ( X1 is everywhere_dense or X2 is everywhere_dense ) holds
X1 union X2 is everywhere_dense SubSpace of X
proof
let X be non empty TopSpace; ::_thesis: for X1, X2 being non empty SubSpace of X st ( X1 is everywhere_dense or X2 is everywhere_dense ) holds
X1 union X2 is everywhere_dense SubSpace of X
let X1, X2 be non empty SubSpace of X; ::_thesis: ( ( X1 is everywhere_dense or X2 is everywhere_dense ) implies X1 union X2 is everywhere_dense SubSpace of X )
reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
reconsider A = the carrier of (X1 union X2) as Subset of X by TSEP_1:1;
assume  ( X1 is everywhere_dense or X2 is everywhere_dense ) ; ::_thesis: X1 union X2 is everywhere_dense SubSpace of X
then  ( A1 is everywhere_dense or A2 is everywhere_dense ) by Def2;
then  A1 \/ A2 is everywhere_dense by TOPS_3:43;
then  A is everywhere_dense by TSEP_1:def_2;
hence  X1 union X2 is everywhere_dense SubSpace of X by Th16; ::_thesis: verum
end;

theorem :: TEX_3:27
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1 is everywhere_dense & X2 is everywhere_dense holds
X1 meet X2 is everywhere_dense SubSpace of X
proof
let X be non empty TopSpace; ::_thesis: for X1, X2 being non empty SubSpace of X st X1 is everywhere_dense & X2 is everywhere_dense holds
X1 meet X2 is everywhere_dense SubSpace of X
let X1, X2 be non empty SubSpace of X; ::_thesis: ( X1 is everywhere_dense & X2 is everywhere_dense implies X1 meet X2 is everywhere_dense SubSpace of X )
reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
reconsider A = the carrier of (X1 meet X2) as Subset of X by TSEP_1:1;
assume  ( X1 is everywhere_dense & X2 is everywhere_dense ) ; ::_thesis: X1 meet X2 is everywhere_dense SubSpace of X
then A1: ( A1 is everywhere_dense & A2 is everywhere_dense ) by Th16;
then  A1 meets A2 by Lm1;
then A2: X1 meets X2 by TSEP_1:def_3;
 A1 /\ A2 is everywhere_dense by A1, TOPS_3:44;
then  A is everywhere_dense by A2, TSEP_1:def_4;
hence  X1 meet X2 is everywhere_dense SubSpace of X by Th16; ::_thesis: verum
end;

theorem :: TEX_3:28
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st ( ( X1 is everywhere_dense & X2 is dense ) or ( X1 is dense & X2 is everywhere_dense ) ) holds
X1 meet X2 is dense SubSpace of X
proof
let X be non empty TopSpace; ::_thesis: for X1, X2 being non empty SubSpace of X st ( ( X1 is everywhere_dense & X2 is dense ) or ( X1 is dense & X2 is everywhere_dense ) ) holds
X1 meet X2 is dense SubSpace of X
let X1, X2 be non empty SubSpace of X; ::_thesis: ( ( ( X1 is everywhere_dense & X2 is dense ) or ( X1 is dense & X2 is everywhere_dense ) ) implies X1 meet X2 is dense SubSpace of X )
reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
reconsider A = the carrier of (X1 meet X2) as Subset of X by TSEP_1:1;
assume  ( ( X1 is everywhere_dense & X2 is dense ) or ( X1 is dense & X2 is everywhere_dense ) ) ; ::_thesis: X1 meet X2 is dense SubSpace of X
then A1: ( ( A1 is everywhere_dense & A2 is dense ) or ( A1 is dense & A2 is everywhere_dense ) ) by Th9, Th16;
then  A1 meets A2 by Lm2;
then A2: X1 meets X2 by TSEP_1:def_3;
 A1 /\ A2 is dense by A1, TOPS_3:45;
then  A is dense by A2, TSEP_1:def_4;
hence  X1 meet X2 is dense SubSpace of X by Th9; ::_thesis: verum
end;

begin

definition
let X be non empty TopSpace;
let IT be SubSpace of X;
attrIT is boundary  means :Def3: :: TEX_3:def 3
 for A being Subset of X st A = the carrier of IT holds
A is boundary ;
end;

:: deftheorem Def3 defines boundary TEX_3:def_3_:_
 for X being non empty TopSpace
for IT being SubSpace of X holds
( IT is boundary iff for A being Subset of X st A = the carrier of IT holds
A is boundary );

theorem Th29: :: TEX_3:29
for X being non empty TopSpace
for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is boundary iff A is boundary )
proof
let X be non empty TopSpace; ::_thesis: for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is boundary iff A is boundary )
let X0 be SubSpace of X; ::_thesis: for A being Subset of X st A = the carrier of X0 holds
( X0 is boundary iff A is boundary )
let A be Subset of X; ::_thesis: ( A = the carrier of X0 implies ( X0 is boundary iff A is boundary ) )
assume A1: A = the carrier of X0 ; ::_thesis: ( X0 is boundary iff A is boundary )
hence  ( X0 is boundary implies A is boundary ) by Def3; ::_thesis: ( A is boundary implies X0 is boundary )
assume  A is boundary ; ::_thesis: X0 is boundary
then  for B being Subset of X st B = the carrier of X0 holds
B is boundary by A1;
hence  X0 is boundary by Def3; ::_thesis: verum
end;

registration
let X be non empty TopSpace;
cluster non empty open  ->  non empty non boundary for SubSpace of X;
coherence
 for b1 being non empty SubSpace of X st b1 is open holds
not b1 is boundary
proof
let X0 be non empty SubSpace of X; ::_thesis: ( X0 is open implies not X0 is boundary )
assume A1: X0 is open ; ::_thesis: not X0 is boundary
now__::_thesis:_not_X0_is_boundary
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
assume  X0 is boundary ; ::_thesis: contradiction
then  A is boundary by Def3;
then A2: Int A = {} ;
 A is open by A1, TSEP_1:16;
hence  contradiction by A2, TOPS_1:23; ::_thesis: verum
end;
hence  not X0 is boundary ; ::_thesis: verum
end;
cluster non empty boundary  ->  non empty non open for SubSpace of X;
coherence
 for b1 being non empty SubSpace of X st b1 is boundary holds
not b1 is open ;
cluster everywhere_dense  ->  non boundary for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is everywhere_dense holds
not b1 is boundary
proof
let X0 be SubSpace of X; ::_thesis: ( X0 is everywhere_dense implies not X0 is boundary )
assume A3: X0 is everywhere_dense ; ::_thesis: not X0 is boundary
now__::_thesis:_not_X0_is_boundary
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
 A is everywhere_dense by A3, Def2;
then A4: not A is boundary by TOPS_3:37;
assume  X0 is boundary ; ::_thesis: contradiction
hence  contradiction by A4, Def3; ::_thesis: verum
end;
hence  not X0 is boundary ; ::_thesis: verum
end;
cluster boundary  ->  non everywhere_dense for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is boundary holds
not b1 is everywhere_dense ;
end;

theorem Th30: :: TEX_3:30
for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is boundary holds
ex X0 being strict SubSpace of X st
( X0 is boundary & A0 = the carrier of X0 )
proof
let X be non empty TopSpace; ::_thesis: for A0 being non empty Subset of X st A0 is boundary holds
ex X0 being strict SubSpace of X st
( X0 is boundary & A0 = the carrier of X0 )
let A0 be non empty Subset of X; ::_thesis: ( A0 is boundary implies ex X0 being strict SubSpace of X st
( X0 is boundary & A0 = the carrier of X0 ) )
assume A1: A0 is boundary ; ::_thesis: ex X0 being strict SubSpace of X st
( X0 is boundary & 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 boundary & A0 = the carrier of X0 )
thus  ( X0 is boundary & A0 = the carrier of X0 ) by A1, A2, Th29; ::_thesis: verum
end;

theorem Th31: :: TEX_3:31
for X being non empty TopSpace
for X1, X2 being SubSpace of X st X1,X2 constitute_a_decomposition holds
( X1 is dense iff X2 is boundary )
proof
let X be non empty TopSpace; ::_thesis: for X1, X2 being SubSpace of X st X1,X2 constitute_a_decomposition holds
( X1 is dense iff X2 is boundary )
let X1, X2 be SubSpace of X; ::_thesis: ( X1,X2 constitute_a_decomposition implies ( X1 is dense iff X2 is boundary ) )
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1:1;
assume A1: for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 constitute_a_decomposition ; :: according to TSEP_2:def_2 ::_thesis: ( X1 is dense iff X2 is boundary )
thus  ( X1 is dense implies X2 is boundary ) ::_thesis: ( X2 is boundary implies X1 is dense )
proof
assume A2: for A1 being Subset of X st A1 = the carrier of X1 holds
A1 is dense ; :: according to TEX_3:def_1 ::_thesis: X2 is boundary
now__::_thesis:_for_A2_being_Subset_of_X_st_A2_=_the_carrier_of_X2_holds_
A2_is_boundary
let A2 be Subset of X; ::_thesis: ( A2 = the carrier of X2 implies A2 is boundary )
assume  A2 = the carrier of X2 ; ::_thesis: A2 is boundary
then A3: A1,A2 constitute_a_decomposition by A1;
 A1 is dense by A2;
hence  A2 is boundary by A3, Th2; ::_thesis: verum
end;
hence  X2 is boundary by Def3; ::_thesis: verum
end;
assume A4: for A2 being Subset of X st A2 = the carrier of X2 holds
A2 is boundary ; :: according to TEX_3:def_3 ::_thesis: X1 is dense
now__::_thesis:_for_A1_being_Subset_of_X_st_A1_=_the_carrier_of_X1_holds_
A1_is_dense
let A1 be Subset of X; ::_thesis: ( A1 = the carrier of X1 implies A1 is dense )
assume  A1 = the carrier of X1 ; ::_thesis: A1 is dense
then A5: A1,A2 constitute_a_decomposition by A1;
 A2 is boundary by A4;
hence  A1 is dense by A5, Th2; ::_thesis: verum
end;
hence  X1 is dense by Def1; ::_thesis: verum
end;

theorem :: TEX_3:32
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1,X2 constitute_a_decomposition holds
( X1 is boundary iff X2 is dense ) by Th31;

theorem Th33: :: TEX_3:33
for X being non empty TopSpace
for X0 being SubSpace of X st X0 is boundary holds
for A being Subset of X st A c= the carrier of X0 holds
A is boundary
proof
let X be non empty TopSpace; ::_thesis: for X0 being SubSpace of X st X0 is boundary holds
for A being Subset of X st A c= the carrier of X0 holds
A is boundary
let X0 be SubSpace of X; ::_thesis: ( X0 is boundary implies for A being Subset of X st A c= the carrier of X0 holds
A is boundary )
reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
assume  X0 is boundary ; ::_thesis: for A being Subset of X st A c= the carrier of X0 holds
A is boundary
then A1: C is boundary by Def3;
let A be Subset of X; ::_thesis: ( A c= the carrier of X0 implies A is boundary )
assume  A c= the carrier of X0 ; ::_thesis: A is boundary
hence  A is boundary by A1, TOPS_3:11; ::_thesis: verum
end;

theorem Th34: :: TEX_3:34
for X being non empty TopSpace
for X1, X2 being SubSpace of X st X1 is boundary & X2 is SubSpace of X1 holds
X2 is boundary
proof
let X be non empty TopSpace; ::_thesis: for X1, X2 being SubSpace of X st X1 is boundary & X2 is SubSpace of X1 holds
X2 is boundary
let X1, X2 be SubSpace of X; ::_thesis: ( X1 is boundary & X2 is SubSpace of X1 implies X2 is boundary )
assume A1: X1 is boundary ; ::_thesis: ( not X2 is SubSpace of X1 or X2 is boundary )
assume  X2 is SubSpace of X1 ; ::_thesis: X2 is boundary
then  the carrier of X2 c= the carrier of X1 by TSEP_1:4;
then  for A being Subset of X st A = the carrier of X2 holds
A is boundary by A1, Th33;
hence  X2 is boundary by Def3; ::_thesis: verum
end;

definition
let X be non empty TopSpace;
let IT be SubSpace of X;
attrIT is nowhere_dense  means :Def4: :: TEX_3:def 4
 for A being Subset of X st A = the carrier of IT holds
A is nowhere_dense ;
end;

:: deftheorem Def4 defines nowhere_dense TEX_3:def_4_:_
 for X being non empty TopSpace
for IT being SubSpace of X holds
( IT is nowhere_dense iff for A being Subset of X st A = the carrier of IT holds
A is nowhere_dense );

theorem Th35: :: TEX_3:35
for X being non empty TopSpace
for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is nowhere_dense iff A is nowhere_dense )
proof
let X be non empty TopSpace; ::_thesis: for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is nowhere_dense iff A is nowhere_dense )
let X0 be SubSpace of X; ::_thesis: for A being Subset of X st A = the carrier of X0 holds
( X0 is nowhere_dense iff A is nowhere_dense )
let A be Subset of X; ::_thesis: ( A = the carrier of X0 implies ( X0 is nowhere_dense iff A is nowhere_dense ) )
assume A1: A = the carrier of X0 ; ::_thesis: ( X0 is nowhere_dense iff A is nowhere_dense )
hence  ( X0 is nowhere_dense implies A is nowhere_dense ) by Def4; ::_thesis: ( A is nowhere_dense implies X0 is nowhere_dense )
assume  A is nowhere_dense ; ::_thesis: X0 is nowhere_dense
then  for B being Subset of X st B = the carrier of X0 holds
B is nowhere_dense by A1;
hence  X0 is nowhere_dense by Def4; ::_thesis: verum
end;

registration
let X be non empty TopSpace;
cluster nowhere_dense  ->  boundary for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is nowhere_dense holds
b1 is boundary
proof
let X0 be SubSpace of X; ::_thesis: ( X0 is nowhere_dense implies X0 is boundary )
assume A1: X0 is nowhere_dense ; ::_thesis: X0 is boundary
now__::_thesis:_for_A_being_Subset_of_X_st_A_=_the_carrier_of_X0_holds_
A_is_boundary
let A be Subset of X; ::_thesis: ( A = the carrier of X0 implies A is boundary )
assume  A = the carrier of X0 ; ::_thesis: A is boundary
then  A is nowhere_dense by A1, Def4;
hence  A is boundary ; ::_thesis: verum
end;
hence  X0 is boundary by Def3; ::_thesis: verum
end;
cluster non boundary  ->  non nowhere_dense for SubSpace of X;
coherence
 for b1 being SubSpace of X st not b1 is boundary holds
not b1 is nowhere_dense ;
cluster nowhere_dense  ->  non dense for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is nowhere_dense holds
not b1 is dense
proof
let X0 be SubSpace of X; ::_thesis: ( X0 is nowhere_dense implies not X0 is dense )
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
assume  X0 is nowhere_dense ; ::_thesis: not X0 is dense
then  A is nowhere_dense by Def4;
then A2: not A is dense by TOPS_3:25;
assume  X0 is dense ; ::_thesis: contradiction
hence  contradiction by A2, Def1; ::_thesis: verum
end;
cluster dense  ->  non nowhere_dense for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is dense holds
not b1 is nowhere_dense ;
end;

theorem :: TEX_3:36
for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is nowhere_dense holds
ex X0 being strict SubSpace of X st
( X0 is nowhere_dense & A0 = the carrier of X0 )
proof
let X be non empty TopSpace; ::_thesis: for A0 being non empty Subset of X st A0 is nowhere_dense holds
ex X0 being strict SubSpace of X st
( X0 is nowhere_dense & A0 = the carrier of X0 )
let A0 be non empty Subset of X; ::_thesis: ( A0 is nowhere_dense implies ex X0 being strict SubSpace of X st
( X0 is nowhere_dense & A0 = the carrier of X0 ) )
assume A1: A0 is nowhere_dense ; ::_thesis: ex X0 being strict SubSpace of X st
( X0 is nowhere_dense & 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 nowhere_dense & A0 = the carrier of X0 )
thus  ( X0 is nowhere_dense & A0 = the carrier of X0 ) by A1, A2, Th35; ::_thesis: verum
end;

theorem Th37: :: TEX_3:37
for X being non empty TopSpace
for X1, X2 being SubSpace of X st X1,X2 constitute_a_decomposition holds
( X1 is everywhere_dense iff X2 is nowhere_dense )
proof
let X be non empty TopSpace; ::_thesis: for X1, X2 being SubSpace of X st X1,X2 constitute_a_decomposition holds
( X1 is everywhere_dense iff X2 is nowhere_dense )
let X1, X2 be SubSpace of X; ::_thesis: ( X1,X2 constitute_a_decomposition implies ( X1 is everywhere_dense iff X2 is nowhere_dense ) )
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1:1;
assume A1: for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 constitute_a_decomposition ; :: according to TSEP_2:def_2 ::_thesis: ( X1 is everywhere_dense iff X2 is nowhere_dense )
thus  ( X1 is everywhere_dense implies X2 is nowhere_dense ) ::_thesis: ( X2 is nowhere_dense implies X1 is everywhere_dense )
proof
assume A2: for A1 being Subset of X st A1 = the carrier of X1 holds
A1 is everywhere_dense ; :: according to TEX_3:def_2 ::_thesis: X2 is nowhere_dense
now__::_thesis:_for_A2_being_Subset_of_X_st_A2_=_the_carrier_of_X2_holds_
A2_is_nowhere_dense
let A2 be Subset of X; ::_thesis: ( A2 = the carrier of X2 implies A2 is nowhere_dense )
assume  A2 = the carrier of X2 ; ::_thesis: A2 is nowhere_dense
then A3: A1,A2 constitute_a_decomposition by A1;
 A1 is everywhere_dense by A2;
hence  A2 is nowhere_dense by A3, Th4; ::_thesis: verum
end;
hence  X2 is nowhere_dense by Def4; ::_thesis: verum
end;
assume A4: for A2 being Subset of X st A2 = the carrier of X2 holds
A2 is nowhere_dense ; :: according to TEX_3:def_4 ::_thesis: X1 is everywhere_dense
now__::_thesis:_for_A1_being_Subset_of_X_st_A1_=_the_carrier_of_X1_holds_
A1_is_everywhere_dense
let A1 be Subset of X; ::_thesis: ( A1 = the carrier of X1 implies A1 is everywhere_dense )
assume  A1 = the carrier of X1 ; ::_thesis: A1 is everywhere_dense
then A5: A1,A2 constitute_a_decomposition by A1;
 A2 is nowhere_dense by A4;
hence  A1 is everywhere_dense by A5, Th4; ::_thesis: verum
end;
hence  X1 is everywhere_dense by Def2; ::_thesis: verum
end;

theorem :: TEX_3:38
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1,X2 constitute_a_decomposition holds
( X1 is nowhere_dense iff X2 is everywhere_dense ) by Th37;

theorem Th39: :: TEX_3:39
for X being non empty TopSpace
for X0 being SubSpace of X st X0 is nowhere_dense holds
for A being Subset of X st A c= the carrier of X0 holds
A is nowhere_dense
proof
let X be non empty TopSpace; ::_thesis: for X0 being SubSpace of X st X0 is nowhere_dense holds
for A being Subset of X st A c= the carrier of X0 holds
A is nowhere_dense
let X0 be SubSpace of X; ::_thesis: ( X0 is nowhere_dense implies for A being Subset of X st A c= the carrier of X0 holds
A is nowhere_dense )
reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
assume  X0 is nowhere_dense ; ::_thesis: for A being Subset of X st A c= the carrier of X0 holds
A is nowhere_dense
then A1: C is nowhere_dense by Def4;
let A be Subset of X; ::_thesis: ( A c= the carrier of X0 implies A is nowhere_dense )
assume  A c= the carrier of X0 ; ::_thesis: A is nowhere_dense
hence  A is nowhere_dense by A1, TOPS_3:26; ::_thesis: verum
end;

theorem Th40: :: TEX_3:40
for X being non empty TopSpace
for X1, X2 being SubSpace of X st X1 is nowhere_dense & X2 is SubSpace of X1 holds
X2 is nowhere_dense
proof
let X be non empty TopSpace; ::_thesis: for X1, X2 being SubSpace of X st X1 is nowhere_dense & X2 is SubSpace of X1 holds
X2 is nowhere_dense
let X1, X2 be SubSpace of X; ::_thesis: ( X1 is nowhere_dense & X2 is SubSpace of X1 implies X2 is nowhere_dense )
assume A1: X1 is nowhere_dense ; ::_thesis: ( not X2 is SubSpace of X1 or X2 is nowhere_dense )
assume  X2 is SubSpace of X1 ; ::_thesis: X2 is nowhere_dense
then  the carrier of X2 c= the carrier of X1 by TSEP_1:4;
then  for A being Subset of X st A = the carrier of X2 holds
A is nowhere_dense by A1, Th39;
hence  X2 is nowhere_dense by Def4; ::_thesis: verum
end;

registration
let X be non empty TopSpace;
cluster closed boundary  ->  nowhere_dense for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is boundary & b1 is closed holds
b1 is nowhere_dense
proof
let X0 be SubSpace of X; ::_thesis: ( X0 is boundary & X0 is closed implies X0 is nowhere_dense )
assume A1: ( X0 is boundary & X0 is closed ) ; ::_thesis: X0 is nowhere_dense
now__::_thesis:_for_A_being_Subset_of_X_st_A_=_the_carrier_of_X0_holds_
A_is_nowhere_dense
let A be Subset of X; ::_thesis: ( A = the carrier of X0 implies A is nowhere_dense )
assume  A = the carrier of X0 ; ::_thesis: A is nowhere_dense
then  ( A is boundary & A is closed ) by A1, Th29, TSEP_1:11;
hence  A is nowhere_dense ; ::_thesis: verum
end;
hence  X0 is nowhere_dense by Def4; ::_thesis: verum
end;
cluster boundary non nowhere_dense  ->  non closed for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is boundary & not b1 is nowhere_dense holds
not b1 is closed ;
cluster closed non nowhere_dense  ->  non boundary for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is closed & not b1 is nowhere_dense holds
not b1 is boundary ;
end;

theorem Th41: :: TEX_3:41
for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is boundary & A0 is closed holds
ex X0 being non empty strict closed SubSpace of X st
( X0 is boundary & A0 = the carrier of X0 )
proof
let X be non empty TopSpace; ::_thesis: for A0 being non empty Subset of X st A0 is boundary & A0 is closed holds
ex X0 being non empty strict closed SubSpace of X st
( X0 is boundary & A0 = the carrier of X0 )
let A0 be non empty Subset of X; ::_thesis: ( A0 is boundary & A0 is closed implies ex X0 being non empty strict closed SubSpace of X st
( X0 is boundary & A0 = the carrier of X0 ) )
consider X0 being non empty strict SubSpace of X such that
A1: A0 = the carrier of X0 by TSEP_1:10;
assume A2: ( A0 is boundary & A0 is closed ) ; ::_thesis: ex X0 being non empty strict closed SubSpace of X st
( X0 is boundary & A0 = the carrier of X0 )
then reconsider Y0 = X0 as non empty strict closed SubSpace of X by A1, TSEP_1:11;
take  Y0 ; ::_thesis: ( Y0 is boundary & A0 = the carrier of Y0 )
thus  ( Y0 is boundary & A0 = the carrier of Y0 ) by A2, A1, Th29; ::_thesis: verum
end;

theorem :: TEX_3:42
for X being non empty TopSpace
for X0 being non empty SubSpace of X holds
( X0 is nowhere_dense iff ex X1 being non empty strict closed SubSpace of X st
( X1 is boundary & X0 is SubSpace of X1 ) )
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty SubSpace of X holds
( X0 is nowhere_dense iff ex X1 being non empty strict closed SubSpace of X st
( X1 is boundary & X0 is SubSpace of X1 ) )
let X0 be non empty SubSpace of X; ::_thesis: ( X0 is nowhere_dense iff ex X1 being non empty strict closed SubSpace of X st
( X1 is boundary & X0 is SubSpace of X1 ) )
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
thus  ( X0 is nowhere_dense implies ex X1 being non empty strict closed SubSpace of X st
( X1 is boundary & X0 is SubSpace of X1 ) ) ::_thesis: ( ex X1 being non empty strict closed SubSpace of X st
( X1 is boundary & X0 is SubSpace of X1 ) implies X0 is nowhere_dense )
proof
assume  X0 is nowhere_dense ; ::_thesis: ex X1 being non empty strict closed SubSpace of X st
( X1 is boundary & X0 is SubSpace of X1 )
then  A is nowhere_dense by Def4;
then consider C being Subset of X such that
A1: A c= C and
A2: ( C is closed & C is boundary ) by TOPS_3:27;
 not C is empty by A1, XBOOLE_1:3;
then consider X1 being non empty strict closed SubSpace of X such that
A3: ( X1 is boundary & C = the carrier of X1 ) by A2, Th41;
take  X1 ; ::_thesis: ( X1 is boundary & X0 is SubSpace of X1 )
thus  ( X1 is boundary & X0 is SubSpace of X1 ) by A1, A3, TSEP_1:4; ::_thesis: verum
end;
given X1 being non empty strict closed SubSpace of X such that A4: ( X1 is boundary & X0 is SubSpace of X1 ) ; ::_thesis: X0 is nowhere_dense
reconsider C = the carrier of X1 as Subset of X by TSEP_1:1;
now__::_thesis:_ex_C_being_Subset_of_X_st_
(_A_c=_C_&_C_is_boundary_&_C_is_closed_)
take C = C; ::_thesis: ( A c= C & C is boundary & C is closed )
thus  ( A c= C & C is boundary & C is closed ) by A4, Def3, TSEP_1:4, TSEP_1:11; ::_thesis: verum
end;
then  for A being Subset of X st A = the carrier of X0 holds
A is nowhere_dense by TOPS_3:27;
hence  X0 is nowhere_dense by Def4; ::_thesis: verum
end;


theorem :: TEX_3:43
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st ( X1 is boundary or X2 is boundary ) & X1 meets X2 holds
X1 meet X2 is boundary
proof
let X be non empty TopSpace; ::_thesis: for X1, X2 being non empty SubSpace of X st ( X1 is boundary or X2 is boundary ) & X1 meets X2 holds
X1 meet X2 is boundary
let X1, X2 be non empty SubSpace of X; ::_thesis: ( ( X1 is boundary or X2 is boundary ) & X1 meets X2 implies X1 meet X2 is boundary )
assume A1: ( X1 is boundary or X2 is boundary ) ; ::_thesis: ( not X1 meets X2 or X1 meet X2 is boundary )
assume A2: X1 meets X2 ; ::_thesis: X1 meet X2 is boundary
hereby  ::_thesis: verum
percases ( X1 is boundary or X2 is boundary ) by A1;
supposeA3: X1 is boundary ; ::_thesis: X1 meet X2 is boundary
 X1 meet X2 is SubSpace of X1 by A2, TSEP_1:27;
hence  X1 meet X2 is boundary by A3, Th34; ::_thesis: verum
end;
supposeA4: X2 is boundary ; ::_thesis: X1 meet X2 is boundary
 X1 meet X2 is SubSpace of X2 by A2, TSEP_1:27;
hence  X1 meet X2 is boundary by A4, Th34; ::_thesis: verum
end;
end;
end;
end;

theorem :: TEX_3:44
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1 is nowhere_dense & X2 is nowhere_dense holds
X1 union X2 is nowhere_dense
proof
let X be non empty TopSpace; ::_thesis: for X1, X2 being non empty SubSpace of X st X1 is nowhere_dense & X2 is nowhere_dense holds
X1 union X2 is nowhere_dense
let X1, X2 be non empty SubSpace of X; ::_thesis: ( X1 is nowhere_dense & X2 is nowhere_dense implies X1 union X2 is nowhere_dense )
reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
assume  ( X1 is nowhere_dense & X2 is nowhere_dense ) ; ::_thesis: X1 union X2 is nowhere_dense
then  ( A1 is nowhere_dense & A2 is nowhere_dense ) by Def4;
then  A1 \/ A2 is nowhere_dense by TOPS_1:53;
then  for A being Subset of X st A = the carrier of (X1 union X2) holds
A is nowhere_dense by TSEP_1:def_2;
hence  X1 union X2 is nowhere_dense by Def4; ::_thesis: verum
end;

theorem :: TEX_3:45
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st ( ( X1 is nowhere_dense & X2 is boundary ) or ( X1 is boundary & X2 is nowhere_dense ) ) holds
X1 union X2 is boundary
proof
let X be non empty TopSpace; ::_thesis: for X1, X2 being non empty SubSpace of X st ( ( X1 is nowhere_dense & X2 is boundary ) or ( X1 is boundary & X2 is nowhere_dense ) ) holds
X1 union X2 is boundary
let X1, X2 be non empty SubSpace of X; ::_thesis: ( ( ( X1 is nowhere_dense & X2 is boundary ) or ( X1 is boundary & X2 is nowhere_dense ) ) implies X1 union X2 is boundary )
reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
assume  ( ( X1 is nowhere_dense & X2 is boundary ) or ( X1 is boundary & X2 is nowhere_dense ) ) ; ::_thesis: X1 union X2 is boundary
then  ( ( A1 is nowhere_dense & A2 is boundary ) or ( A1 is boundary & A2 is nowhere_dense ) ) by Def3, Def4;
then  A1 \/ A2 is boundary by TOPS_3:30;
then  for A being Subset of X st A = the carrier of (X1 union X2) holds
A is boundary by TSEP_1:def_2;
hence  X1 union X2 is boundary by Def3; ::_thesis: verum
end;

theorem :: TEX_3:46
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st ( X1 is nowhere_dense or X2 is nowhere_dense ) & X1 meets X2 holds
X1 meet X2 is nowhere_dense
proof
let X be non empty TopSpace; ::_thesis: for X1, X2 being non empty SubSpace of X st ( X1 is nowhere_dense or X2 is nowhere_dense ) & X1 meets X2 holds
X1 meet X2 is nowhere_dense
let X1, X2 be non empty SubSpace of X; ::_thesis: ( ( X1 is nowhere_dense or X2 is nowhere_dense ) & X1 meets X2 implies X1 meet X2 is nowhere_dense )
assume A1: ( X1 is nowhere_dense or X2 is nowhere_dense ) ; ::_thesis: ( not X1 meets X2 or X1 meet X2 is nowhere_dense )
assume A2: X1 meets X2 ; ::_thesis: X1 meet X2 is nowhere_dense
hereby  ::_thesis: verum
percases ( X1 is nowhere_dense or X2 is nowhere_dense ) by A1;
supposeA3: X1 is nowhere_dense ; ::_thesis: X1 meet X2 is nowhere_dense
 X1 meet X2 is SubSpace of X1 by A2, TSEP_1:27;
hence  X1 meet X2 is nowhere_dense by A3, Th40; ::_thesis: verum
end;
supposeA4: X2 is nowhere_dense ; ::_thesis: X1 meet X2 is nowhere_dense
 X1 meet X2 is SubSpace of X2 by A2, TSEP_1:27;
hence  X1 meet X2 is nowhere_dense by A4, Th40; ::_thesis: verum
end;
end;
end;
end;

begin

theorem :: TEX_3:47
for X being non empty TopSpace st ( for X0 being SubSpace of X holds not X0 is boundary ) holds
X is discrete
proof
let X be non empty TopSpace; ::_thesis: ( ( for X0 being SubSpace of X holds not X0 is boundary ) implies X is discrete )
assume A1: for X0 being SubSpace of X holds not X0 is boundary ; ::_thesis: X is discrete
now__::_thesis:_for_A_being_non_empty_Subset_of_X_holds_not_A_is_boundary
let A be non empty Subset of X; ::_thesis: not A is boundary
consider X0 being non empty strict SubSpace of X such that
A2: A = the carrier of X0 by TSEP_1:10;
 not X0 is boundary by A1;
hence  not A is boundary by A2, Th29; ::_thesis: verum
end;
hence  X is discrete by TEX_1:def_5; ::_thesis: verum
end;

theorem :: TEX_3:48
for X being non trivial TopSpace st ( for X0 being proper SubSpace of X holds not X0 is dense ) holds
X is discrete
proof
let X be non trivial TopSpace; ::_thesis: ( ( for X0 being proper SubSpace of X holds not X0 is dense ) implies X is discrete )
assume A1: for X0 being proper SubSpace of X holds not X0 is dense ; ::_thesis: X is discrete
now__::_thesis:_for_A_being_Subset_of_X_st_A_<>_the_carrier_of_X_holds_
not_A_is_dense
let A be Subset of X; ::_thesis: ( A <> the carrier of X implies not A is dense )
assume A2: A <> the carrier of X ; ::_thesis: not A is dense
now__::_thesis:_not_A_is_dense
percases ( A is empty or not A is empty ) ;
suppose A is empty ; ::_thesis: not A is dense
hence  not A is dense by TOPS_3:17; ::_thesis: verum
end;
suppose not A is empty ; ::_thesis: not A is dense
then consider X0 being non empty strict SubSpace of X such that
A3: A = the carrier of X0 by TSEP_1:10;
 A is proper by A2, SUBSET_1:def_6;
then reconsider X0 = X0 as strict proper SubSpace of X by A3, TEX_2:8;
 not X0 is dense by A1;
hence  not A is dense by A3, Th9; ::_thesis: verum
end;
end;
end;
hence  not A is dense ; ::_thesis: verum
end;
hence  X is discrete by TEX_1:31; ::_thesis: verum
end;

registration
let X be non empty discrete TopSpace;
cluster non empty  ->  non empty non boundary for SubSpace of X;
coherence
 for b1 being non empty SubSpace of X holds not b1 is boundary ;
cluster proper  ->  non dense for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is proper holds
not b1 is dense ;
cluster dense  ->  non proper for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is dense holds
not b1 is proper ;
end;

registration
let X be non empty discrete TopSpace;
cluster non empty strict TopSpace-like closed open discrete almost_discrete non boundary for SubSpace of X;
existence
 ex b1 being SubSpace of X st
( not b1 is boundary & b1 is strict & not b1 is empty )
proof
set X0 = the non empty strict SubSpace of X;
take  the non empty strict SubSpace of X ; ::_thesis: ( not the non empty strict SubSpace of X is boundary & the non empty strict SubSpace of X is strict & not the non empty strict SubSpace of X is empty )
thus  ( not the non empty strict SubSpace of X is boundary & the non empty strict SubSpace of X is strict & not the non empty strict SubSpace of X is empty ) ; ::_thesis: verum
end;
end;

registration
let X be non trivial discrete TopSpace;
cluster strict TopSpace-like closed open discrete almost_discrete non dense for SubSpace of X;
existence
 ex b1 being SubSpace of X st
( not b1 is dense & b1 is strict )
proof
set X0 = the strict proper SubSpace of X;
take  the strict proper SubSpace of X ; ::_thesis: ( not the strict proper SubSpace of X is dense & the strict proper SubSpace of X is strict )
thus  ( not the strict proper SubSpace of X is dense & the strict proper SubSpace of X is strict ) ; ::_thesis: verum
end;
end;

theorem :: TEX_3:49
for X being non empty TopSpace st ex X0 being non empty SubSpace of X st X0 is boundary holds
not X is discrete ;

theorem :: TEX_3:50
for X being non empty TopSpace st ex X0 being non empty SubSpace of X st
( X0 is dense & X0 is proper ) holds
not X is discrete ;

registration
let X be non empty non discrete TopSpace;
cluster non empty strict TopSpace-like boundary for SubSpace of X;
existence
 ex b1 being SubSpace of X st
( b1 is boundary & b1 is strict & not b1 is empty )
proof
consider A0 being non empty Subset of X such that
A1: A0 is boundary by TEX_1:def_5;
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 boundary & X0 is strict & not X0 is empty )
 for A being Subset of X st A = the carrier of X0 holds
A is boundary by A1, A2;
hence  ( X0 is boundary & X0 is strict & not X0 is empty ) by Def3; ::_thesis: verum
end;
cluster non empty strict TopSpace-like proper dense for SubSpace of X;
existence
 ex b1 being SubSpace of X st
( b1 is dense & b1 is proper & b1 is strict & not b1 is empty )
proof
consider A0 being Subset of X such that
A3: A0 <> the carrier of X and
A4: A0 is dense by TEX_1:31;
 not A0 is empty by A4, TOPS_3:17;
then consider X0 being non empty strict dense SubSpace of X such that
A5: A0 = the carrier of X0 by A4, Th10;
take  X0 ; ::_thesis: ( X0 is dense & X0 is proper & X0 is strict & not X0 is empty )
 A0 is proper by A3, SUBSET_1:def_6;
hence  ( X0 is dense & X0 is proper & X0 is strict & not X0 is empty ) by A5, TEX_2:8; ::_thesis: verum
end;
end;

theorem :: TEX_3:51
for X being non empty non discrete TopSpace
for A0 being non empty Subset of X st A0 is boundary holds
ex X0 being strict boundary SubSpace of X st A0 = the carrier of X0
proof
let X be non empty non discrete TopSpace; ::_thesis: for A0 being non empty Subset of X st A0 is boundary holds
ex X0 being strict boundary SubSpace of X st A0 = the carrier of X0
let A0 be non empty Subset of X; ::_thesis: ( A0 is boundary implies ex X0 being strict boundary SubSpace of X st A0 = the carrier of X0 )
assume  A0 is boundary ; ::_thesis: ex X0 being strict boundary SubSpace of X st A0 = the carrier of X0
then  ex X0 being strict SubSpace of X st
( X0 is boundary & A0 = the carrier of X0 ) by Th30;
hence  ex X0 being strict boundary SubSpace of X st A0 = the carrier of X0 ; ::_thesis: verum
end;

theorem :: TEX_3:52
for X being non empty non discrete TopSpace
for A0 being non empty proper Subset of X st A0 is dense holds
ex X0 being strict proper dense SubSpace of X st A0 = the carrier of X0
proof
let X be non empty non discrete TopSpace; ::_thesis: for A0 being non empty proper Subset of X st A0 is dense holds
ex X0 being strict proper dense SubSpace of X st A0 = the carrier of X0
let A0 be non empty proper Subset of X; ::_thesis: ( A0 is dense implies ex X0 being strict proper dense SubSpace of X st A0 = the carrier of X0 )
consider X0 being non empty strict SubSpace of X such that
A1: A0 = the carrier of X0 by TSEP_1:10;
assume  A0 is dense ; ::_thesis: ex X0 being strict proper dense SubSpace of X st A0 = the carrier of X0
then reconsider X0 = X0 as strict proper dense SubSpace of X by A1, Th9, TEX_2:8;
take  X0 ; ::_thesis: A0 = the carrier of X0
thus  A0 = the carrier of X0 by A1; ::_thesis: verum
end;

theorem :: TEX_3:53
for X being non empty non discrete TopSpace
for X1 being non empty boundary SubSpace of X ex X2 being non empty strict proper dense SubSpace of X st X1,X2 constitute_a_decomposition
proof
let X be non empty non discrete TopSpace; ::_thesis: for X1 being non empty boundary SubSpace of X ex X2 being non empty strict proper dense SubSpace of X st X1,X2 constitute_a_decomposition
let X1 be non empty boundary SubSpace of X; ::_thesis: ex X2 being non empty strict proper dense SubSpace of X st X1,X2 constitute_a_decomposition
consider X2 being non empty strict proper SubSpace of X such that
A1: X1,X2 constitute_a_decomposition by Th8;
reconsider X2 = X2 as non empty strict proper dense SubSpace of X by A1, Th31;
take  X2 ; ::_thesis: X1,X2 constitute_a_decomposition
thus  X1,X2 constitute_a_decomposition by A1; ::_thesis: verum
end;

theorem :: TEX_3:54
for X being non empty non discrete TopSpace
for X1 being non empty proper dense SubSpace of X ex X2 being non empty strict boundary SubSpace of X st X1,X2 constitute_a_decomposition
proof
let X be non empty non discrete TopSpace; ::_thesis: for X1 being non empty proper dense SubSpace of X ex X2 being non empty strict boundary SubSpace of X st X1,X2 constitute_a_decomposition
let X1 be non empty proper dense SubSpace of X; ::_thesis: ex X2 being non empty strict boundary SubSpace of X st X1,X2 constitute_a_decomposition
consider X2 being non empty strict proper SubSpace of X such that
A1: X1,X2 constitute_a_decomposition by Th8;
reconsider X2 = X2 as non empty strict boundary SubSpace of X by A1, Th31;
take  X2 ; ::_thesis: X1,X2 constitute_a_decomposition
thus  X1,X2 constitute_a_decomposition by A1; ::_thesis: verum
end;

theorem :: TEX_3:55
for X being non empty non discrete TopSpace
for Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1, the topology of Y1 #) holds
( Y1 is boundary SubSpace of X iff Y2 is boundary SubSpace of X )
proof
let X be non empty non discrete TopSpace; ::_thesis: for Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1, the topology of Y1 #) holds
( Y1 is boundary SubSpace of X iff Y2 is boundary SubSpace of X )
let X1, X2 be non empty TopSpace; ::_thesis: ( X2 = TopStruct(# the carrier of X1, the topology of X1 #) implies ( X1 is boundary SubSpace of X iff X2 is boundary SubSpace of X ) )
assume A1: X2 = TopStruct(# the carrier of X1, the topology of X1 #) ; ::_thesis: ( X1 is boundary SubSpace of X iff X2 is boundary SubSpace of X )
thus  ( X1 is boundary SubSpace of X implies X2 is boundary SubSpace of X ) ::_thesis: ( X2 is boundary SubSpace of X implies X1 is boundary SubSpace of X )
proof
assume A2: X1 is boundary SubSpace of X ; ::_thesis: X2 is boundary SubSpace of X
then reconsider Y2 = X2 as SubSpace of X by A1, TMAP_1:7;
 for A2 being Subset of X st A2 = the carrier of Y2 holds
A2 is boundary by A1, A2, Def3;
hence  X2 is boundary SubSpace of X by Def3; ::_thesis: verum
end;
assume A3: X2 is boundary SubSpace of X ; ::_thesis: X1 is boundary SubSpace of X
then reconsider Y1 = X1 as SubSpace of X by A1, TMAP_1:7;
 for A1 being Subset of X st A1 = the carrier of Y1 holds
A1 is boundary by A1, A3, Def3;
hence  X1 is boundary SubSpace of X by Def3; ::_thesis: verum
end;

begin

theorem :: TEX_3:56
for X being non empty TopSpace st ( for X0 being SubSpace of X holds not X0 is nowhere_dense ) holds
X is almost_discrete
proof
let X be non empty TopSpace; ::_thesis: ( ( for X0 being SubSpace of X holds not X0 is nowhere_dense ) implies X is almost_discrete )
assume A1: for X0 being SubSpace of X holds not X0 is nowhere_dense ; ::_thesis: X is almost_discrete
now__::_thesis:_for_A_being_non_empty_Subset_of_X_holds_not_A_is_nowhere_dense
let A be non empty Subset of X; ::_thesis: not A is nowhere_dense
consider X0 being non empty strict SubSpace of X such that
A2: A = the carrier of X0 by TSEP_1:10;
 not X0 is nowhere_dense by A1;
hence  not A is nowhere_dense by A2, Th35; ::_thesis: verum
end;
hence  X is almost_discrete by TEX_1:def_6; ::_thesis: verum
end;

theorem :: TEX_3:57
for X being non trivial TopSpace st ( for X0 being proper SubSpace of X holds not X0 is everywhere_dense ) holds
X is almost_discrete
proof
let X be non trivial TopSpace; ::_thesis: ( ( for X0 being proper SubSpace of X holds not X0 is everywhere_dense ) implies X is almost_discrete )
assume A1: for X0 being proper SubSpace of X holds not X0 is everywhere_dense ; ::_thesis: X is almost_discrete
now__::_thesis:_for_A_being_Subset_of_X_st_A_<>_the_carrier_of_X_holds_
not_A_is_everywhere_dense
let A be Subset of X; ::_thesis: ( A <> the carrier of X implies not A is everywhere_dense )
assume A2: A <> the carrier of X ; ::_thesis: not A is everywhere_dense
now__::_thesis:_not_A_is_everywhere_dense
percases ( A is empty or not A is empty ) ;
suppose A is empty ; ::_thesis: not A is everywhere_dense
hence  not A is everywhere_dense by TOPS_3:34; ::_thesis: verum
end;
suppose not A is empty ; ::_thesis: not A is everywhere_dense
then consider X0 being non empty strict SubSpace of X such that
A3: A = the carrier of X0 by TSEP_1:10;
 A is proper by A2, SUBSET_1:def_6;
then reconsider X0 = X0 as strict proper SubSpace of X by A3, TEX_2:8;
 not X0 is everywhere_dense by A1;
hence  not A is everywhere_dense by A3, Th16; ::_thesis: verum
end;
end;
end;
hence  not A is everywhere_dense ; ::_thesis: verum
end;
hence  X is almost_discrete by TEX_1:32; ::_thesis: verum
end;

registration
let X be non empty almost_discrete TopSpace;
cluster non empty  ->  non empty non nowhere_dense for SubSpace of X;
coherence
 for b1 being non empty SubSpace of X holds not b1 is nowhere_dense
proof
let X0 be non empty SubSpace of X; ::_thesis: not X0 is nowhere_dense
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
 not A is nowhere_dense by TEX_1:def_6;
hence  not X0 is nowhere_dense by Th35; ::_thesis: verum
end;
cluster proper  ->  non everywhere_dense for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is proper holds
not b1 is everywhere_dense
proof
let X0 be SubSpace of X; ::_thesis: ( X0 is proper implies not X0 is everywhere_dense )
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
assume  X0 is proper ; ::_thesis: not X0 is everywhere_dense
then  A is proper by TEX_2:8;
then  A <> the carrier of X by SUBSET_1:def_6;
then  not A is everywhere_dense by TEX_1:32;
hence  not X0 is everywhere_dense by Th16; ::_thesis: verum
end;
cluster everywhere_dense  ->  non proper for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is everywhere_dense holds
not b1 is proper ;
cluster non empty boundary  ->  non empty non closed for SubSpace of X;
coherence
 for b1 being non empty SubSpace of X st b1 is boundary holds
not b1 is closed ;
cluster non empty closed  ->  non empty non boundary for SubSpace of X;
coherence
 for b1 being non empty SubSpace of X st b1 is closed holds
not b1 is boundary ;
cluster proper dense  ->  non open for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is dense & b1 is proper holds
not b1 is open ;
cluster open dense  ->  non proper for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is dense & b1 is open holds
not b1 is proper ;
cluster open proper  ->  non dense for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is open & b1 is proper holds
not b1 is dense ;
end;

registration
let X be non empty almost_discrete TopSpace;
cluster non empty strict TopSpace-like non nowhere_dense for SubSpace of X;
existence
 ex b1 being SubSpace of X st
( not b1 is nowhere_dense & b1 is strict & not b1 is empty )
proof
set X0 = the non empty strict SubSpace of X;
take  the non empty strict SubSpace of X ; ::_thesis: ( not the non empty strict SubSpace of X is nowhere_dense & the non empty strict SubSpace of X is strict & not the non empty strict SubSpace of X is empty )
thus  ( not the non empty strict SubSpace of X is nowhere_dense & the non empty strict SubSpace of X is strict & not the non empty strict SubSpace of X is empty ) ; ::_thesis: verum
end;
end;

registration
let X be non trivial almost_discrete TopSpace;
cluster strict TopSpace-like non everywhere_dense for SubSpace of X;
existence
 ex b1 being SubSpace of X st
( not b1 is everywhere_dense & b1 is strict )
proof
set X0 = the strict proper SubSpace of X;
take  the strict proper SubSpace of X ; ::_thesis: ( not the strict proper SubSpace of X is everywhere_dense & the strict proper SubSpace of X is strict )
thus  ( not the strict proper SubSpace of X is everywhere_dense & the strict proper SubSpace of X is strict ) ; ::_thesis: verum
end;
end;

theorem :: TEX_3:58
for X being non empty TopSpace st ex X0 being non empty SubSpace of X st X0 is nowhere_dense holds
not X is almost_discrete ;

theorem :: TEX_3:59
for X being non empty TopSpace st ex X0 being non empty SubSpace of X st
( X0 is boundary & X0 is closed ) holds
not X is almost_discrete ;

theorem :: TEX_3:60
for X being non empty TopSpace st ex X0 being non empty SubSpace of X st
( X0 is everywhere_dense & X0 is proper ) holds
not X is almost_discrete ;

theorem :: TEX_3:61
for X being non empty TopSpace st ex X0 being non empty SubSpace of X st
( X0 is dense & X0 is open & X0 is proper ) holds
not X is almost_discrete ;

registration
let X be non empty non almost_discrete TopSpace;
cluster non empty strict TopSpace-like nowhere_dense for SubSpace of X;
existence
 ex b1 being SubSpace of X st
( b1 is nowhere_dense & b1 is strict & not b1 is empty )
proof
consider A0 being non empty Subset of X such that
A1: A0 is nowhere_dense by TEX_1:def_6;
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 nowhere_dense & X0 is strict & not X0 is empty )
 for A being Subset of X st A = the carrier of X0 holds
A is nowhere_dense by A1, A2;
hence  ( X0 is nowhere_dense & X0 is strict & not X0 is empty ) by Def4; ::_thesis: verum
end;
cluster non empty strict TopSpace-like proper everywhere_dense for SubSpace of X;
existence
 ex b1 being SubSpace of X st
( b1 is everywhere_dense & b1 is proper & b1 is strict & not b1 is empty )
proof
consider A0 being Subset of X such that
A3: A0 <> the carrier of X and
A4: A0 is everywhere_dense by TEX_1:32;
 not A0 is empty by A4, TOPS_3:34;
then consider X0 being non empty strict everywhere_dense SubSpace of X such that
A5: A0 = the carrier of X0 by A4, Th17;
take  X0 ; ::_thesis: ( X0 is everywhere_dense & X0 is proper & X0 is strict & not X0 is empty )
 A0 is proper by A3, SUBSET_1:def_6;
hence  ( X0 is everywhere_dense & X0 is proper & X0 is strict & not X0 is empty ) by A5, TEX_2:8; ::_thesis: verum
end;
end;

theorem Th62: :: TEX_3:62
for X being non empty non almost_discrete TopSpace
for A0 being non empty Subset of X st A0 is nowhere_dense holds
ex X0 being non empty strict nowhere_dense SubSpace of X st A0 = the carrier of X0
proof
let X be non empty non almost_discrete TopSpace; ::_thesis: for A0 being non empty Subset of X st A0 is nowhere_dense holds
ex X0 being non empty strict nowhere_dense SubSpace of X st A0 = the carrier of X0
let A0 be non empty Subset of X; ::_thesis: ( A0 is nowhere_dense implies ex X0 being non empty strict nowhere_dense SubSpace of X st A0 = the carrier of X0 )
consider X0 being non empty strict SubSpace of X such that
A1: A0 = the carrier of X0 by TSEP_1:10;
assume  A0 is nowhere_dense ; ::_thesis: ex X0 being non empty strict nowhere_dense SubSpace of X st A0 = the carrier of X0
then reconsider Y0 = X0 as non empty strict nowhere_dense SubSpace of X by A1, Th35;
take  Y0 ; ::_thesis: A0 = the carrier of Y0
thus  A0 = the carrier of Y0 by A1; ::_thesis: verum
end;

theorem :: TEX_3:63
for X being non empty non almost_discrete TopSpace
for A0 being non empty proper Subset of X st A0 is everywhere_dense holds
ex X0 being strict proper everywhere_dense SubSpace of X st A0 = the carrier of X0
proof
let X be non empty non almost_discrete TopSpace; ::_thesis: for A0 being non empty proper Subset of X st A0 is everywhere_dense holds
ex X0 being strict proper everywhere_dense SubSpace of X st A0 = the carrier of X0
let A0 be non empty proper Subset of X; ::_thesis: ( A0 is everywhere_dense implies ex X0 being strict proper everywhere_dense SubSpace of X st A0 = the carrier of X0 )
assume  A0 is everywhere_dense ; ::_thesis: ex X0 being strict proper everywhere_dense SubSpace of X st A0 = the carrier of X0
then consider X0 being non empty strict everywhere_dense SubSpace of X such that
A1: A0 = the carrier of X0 by Th17;
reconsider X0 = X0 as strict proper everywhere_dense SubSpace of X by A1, TEX_2:8;
take  X0 ; ::_thesis: A0 = the carrier of X0
thus  A0 = the carrier of X0 by A1; ::_thesis: verum
end;

theorem :: TEX_3:64
for X being non empty non almost_discrete TopSpace
for X1 being non empty nowhere_dense SubSpace of X ex X2 being non empty strict proper everywhere_dense SubSpace of X st X1,X2 constitute_a_decomposition
proof
let X be non empty non almost_discrete TopSpace; ::_thesis: for X1 being non empty nowhere_dense SubSpace of X ex X2 being non empty strict proper everywhere_dense SubSpace of X st X1,X2 constitute_a_decomposition
let X1 be non empty nowhere_dense SubSpace of X; ::_thesis: ex X2 being non empty strict proper everywhere_dense SubSpace of X st X1,X2 constitute_a_decomposition
consider X2 being non empty strict proper SubSpace of X such that
A1: X1,X2 constitute_a_decomposition by Th8;
reconsider X2 = X2 as non empty strict proper everywhere_dense SubSpace of X by A1, Th37;
take  X2 ; ::_thesis: X1,X2 constitute_a_decomposition
thus  X1,X2 constitute_a_decomposition by A1; ::_thesis: verum
end;

theorem :: TEX_3:65
for X being non empty non almost_discrete TopSpace
for X1 being non empty proper everywhere_dense SubSpace of X ex X2 being non empty strict nowhere_dense SubSpace of X st X1,X2 constitute_a_decomposition
proof
let X be non empty non almost_discrete TopSpace; ::_thesis: for X1 being non empty proper everywhere_dense SubSpace of X ex X2 being non empty strict nowhere_dense SubSpace of X st X1,X2 constitute_a_decomposition
let X1 be non empty proper everywhere_dense SubSpace of X; ::_thesis: ex X2 being non empty strict nowhere_dense SubSpace of X st X1,X2 constitute_a_decomposition
consider X2 being non empty strict proper SubSpace of X such that
A1: X1,X2 constitute_a_decomposition by Th8;
reconsider X2 = X2 as non empty strict nowhere_dense SubSpace of X by A1, Th37;
take  X2 ; ::_thesis: X1,X2 constitute_a_decomposition
thus  X1,X2 constitute_a_decomposition by A1; ::_thesis: verum
end;

theorem :: TEX_3:66
for X being non empty non almost_discrete TopSpace
for Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1, the topology of Y1 #) holds
( Y1 is nowhere_dense SubSpace of X iff Y2 is nowhere_dense SubSpace of X )
proof
let X be non empty non almost_discrete TopSpace; ::_thesis: for Y1, Y2 being non empty TopSpace st Y2 = TopStruct(# the carrier of Y1, the topology of Y1 #) holds
( Y1 is nowhere_dense SubSpace of X iff Y2 is nowhere_dense SubSpace of X )
let X1, X2 be non empty TopSpace; ::_thesis: ( X2 = TopStruct(# the carrier of X1, the topology of X1 #) implies ( X1 is nowhere_dense SubSpace of X iff X2 is nowhere_dense SubSpace of X ) )
assume A1: X2 = TopStruct(# the carrier of X1, the topology of X1 #) ; ::_thesis: ( X1 is nowhere_dense SubSpace of X iff X2 is nowhere_dense SubSpace of X )
thus  ( X1 is nowhere_dense SubSpace of X implies X2 is nowhere_dense SubSpace of X ) ::_thesis: ( X2 is nowhere_dense SubSpace of X implies X1 is nowhere_dense SubSpace of X )
proof
assume A2: X1 is nowhere_dense SubSpace of X ; ::_thesis: X2 is nowhere_dense SubSpace of X
then reconsider Y2 = X2 as SubSpace of X by A1, TMAP_1:7;
 for A2 being Subset of X st A2 = the carrier of Y2 holds
A2 is nowhere_dense by A1, A2, Def4;
hence  X2 is nowhere_dense SubSpace of X by Def4; ::_thesis: verum
end;
assume A3: X2 is nowhere_dense SubSpace of X ; ::_thesis: X1 is nowhere_dense SubSpace of X
then reconsider Y1 = X1 as SubSpace of X by A1, TMAP_1:7;
 for A1 being Subset of X st A1 = the carrier of Y1 holds
A1 is nowhere_dense by A1, A3, Def4;
hence  X1 is nowhere_dense SubSpace of X by Def4; ::_thesis: verum
end;

registration
let X be non empty non almost_discrete TopSpace;
cluster non empty strict TopSpace-like closed boundary for SubSpace of X;
existence
 ex b1 being SubSpace of X st
( b1 is boundary & b1 is closed & b1 is strict & not b1 is empty )
proof
consider A being non empty Subset of X such that
A1: A is nowhere_dense by TEX_1:def_6;
consider C being Subset of X such that
A2: A c= C and
A3: ( C is closed & C is boundary ) by A1, TOPS_3:27;
 not C is empty by A2, XBOOLE_1:3;
then consider X0 being non empty strict SubSpace of X such that
A4: C = the carrier of X0 by TSEP_1:10;
take  X0 ; ::_thesis: ( X0 is boundary & X0 is closed & X0 is strict & not X0 is empty )
 ( ( for C being Subset of X st C = the carrier of X0 holds
C is boundary ) & ( for C being Subset of X st C = the carrier of X0 holds
C is closed ) ) by A3, A4;
hence  ( X0 is boundary & X0 is closed & X0 is strict & not X0 is empty ) by Def3, BORSUK_1:def_11; ::_thesis: verum
end;
cluster non empty strict TopSpace-like open proper dense for SubSpace of X;
existence
 ex b1 being SubSpace of X st
( b1 is dense & b1 is open & b1 is proper & b1 is strict & not b1 is empty )
proof
consider A0 being Subset of X such that
A5: A0 <> the carrier of X and
A6: ( A0 is dense & A0 is open ) by TEX_1:34;
 not A0 is empty by A6, TOPS_3:17;
then consider X0 being non empty strict open dense SubSpace of X such that
A7: A0 = the carrier of X0 by A6, Th23;
take  X0 ; ::_thesis: ( X0 is dense & X0 is open & X0 is proper & X0 is strict & not X0 is empty )
 A0 is proper by A5, SUBSET_1:def_6;
hence  ( X0 is dense & X0 is open & X0 is proper & X0 is strict & not X0 is empty ) by A7, TEX_2:8; ::_thesis: verum
end;
end;

theorem Th67: :: TEX_3:67
for X being non empty non almost_discrete TopSpace
for A0 being non empty Subset of X st A0 is boundary & A0 is closed holds
ex X0 being non empty strict closed boundary SubSpace of X st A0 = the carrier of X0
proof
let X be non empty non almost_discrete TopSpace; ::_thesis: for A0 being non empty Subset of X st A0 is boundary & A0 is closed holds
ex X0 being non empty strict closed boundary SubSpace of X st A0 = the carrier of X0
let A0 be non empty Subset of X; ::_thesis: ( A0 is boundary & A0 is closed implies ex X0 being non empty strict closed boundary SubSpace of X st A0 = the carrier of X0 )
consider X0 being non empty strict SubSpace of X such that
A1: A0 = the carrier of X0 by TSEP_1:10;
assume  ( A0 is boundary & A0 is closed ) ; ::_thesis: ex X0 being non empty strict closed boundary SubSpace of X st A0 = the carrier of X0
then reconsider Y0 = X0 as non empty strict closed boundary SubSpace of X by A1, Th29, TSEP_1:11;
take  Y0 ; ::_thesis: A0 = the carrier of Y0
thus  A0 = the carrier of Y0 by A1; ::_thesis: verum
end;

theorem :: TEX_3:68
for X being non empty non almost_discrete TopSpace
for A0 being non empty proper Subset of X st A0 is dense & A0 is open holds
ex X0 being strict open proper dense SubSpace of X st A0 = the carrier of X0
proof
let X be non empty non almost_discrete TopSpace; ::_thesis: for A0 being non empty proper Subset of X st A0 is dense & A0 is open holds
ex X0 being strict open proper dense SubSpace of X st A0 = the carrier of X0
let A0 be non empty proper Subset of X; ::_thesis: ( A0 is dense & A0 is open implies ex X0 being strict open proper dense SubSpace of X st A0 = the carrier of X0 )
assume  ( A0 is dense & A0 is open ) ; ::_thesis: ex X0 being strict open proper dense SubSpace of X st A0 = the carrier of X0
then consider X0 being non empty strict open dense SubSpace of X such that
A1: A0 = the carrier of X0 by Th23;
reconsider X0 = X0 as strict open proper dense SubSpace of X by A1, TEX_2:8;
take  X0 ; ::_thesis: A0 = the carrier of X0
thus  A0 = the carrier of X0 by A1; ::_thesis: verum
end;

theorem :: TEX_3:69
for X being non empty non almost_discrete TopSpace
for X1 being non empty closed boundary SubSpace of X ex X2 being non empty strict open proper dense SubSpace of X st X1,X2 constitute_a_decomposition
proof
let X be non empty non almost_discrete TopSpace; ::_thesis: for X1 being non empty closed boundary SubSpace of X ex X2 being non empty strict open proper dense SubSpace of X st X1,X2 constitute_a_decomposition
let X1 be non empty closed boundary SubSpace of X; ::_thesis: ex X2 being non empty strict open proper dense SubSpace of X st X1,X2 constitute_a_decomposition
consider X2 being non empty strict proper SubSpace of X such that
A1: X1,X2 constitute_a_decomposition by Th8;
reconsider X2 = X2 as non empty strict open proper dense SubSpace of X by A1, Th31, TSEP_2:34;
take  X2 ; ::_thesis: X1,X2 constitute_a_decomposition
thus  X1,X2 constitute_a_decomposition by A1; ::_thesis: verum
end;

theorem :: TEX_3:70
for X being non empty non almost_discrete TopSpace
for X1 being non empty open proper dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st X1,X2 constitute_a_decomposition
proof
let X be non empty non almost_discrete TopSpace; ::_thesis: for X1 being non empty open proper dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st X1,X2 constitute_a_decomposition
let X1 be non empty open proper dense SubSpace of X; ::_thesis: ex X2 being non empty strict closed boundary SubSpace of X st X1,X2 constitute_a_decomposition
consider X2 being non empty strict proper SubSpace of X such that
A1: X1,X2 constitute_a_decomposition by Th8;
reconsider X2 = X2 as non empty strict closed boundary SubSpace of X by A1, Th31, TSEP_2:33;
take  X2 ; ::_thesis: X1,X2 constitute_a_decomposition
thus  X1,X2 constitute_a_decomposition by A1; ::_thesis: verum
end;

theorem :: TEX_3:71
for X being non empty non almost_discrete TopSpace
for X0 being non empty SubSpace of X holds
( X0 is nowhere_dense iff ex X1 being non empty strict closed boundary SubSpace of X st X0 is SubSpace of X1 )
proof
let X be non empty non almost_discrete TopSpace; ::_thesis: for X0 being non empty SubSpace of X holds
( X0 is nowhere_dense iff ex X1 being non empty strict closed boundary SubSpace of X st X0 is SubSpace of X1 )
let X0 be non empty SubSpace of X; ::_thesis: ( X0 is nowhere_dense iff ex X1 being non empty strict closed boundary SubSpace of X st X0 is SubSpace of X1 )
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
thus  ( X0 is nowhere_dense implies ex X1 being non empty strict closed boundary SubSpace of X st X0 is SubSpace of X1 ) ::_thesis: ( ex X1 being non empty strict closed boundary SubSpace of X st X0 is SubSpace of X1 implies X0 is nowhere_dense )
proof
assume  X0 is nowhere_dense ; ::_thesis: ex X1 being non empty strict closed boundary SubSpace of X st X0 is SubSpace of X1
then  A is nowhere_dense by Def4;
then consider C being Subset of X such that
A1: A c= C and
A2: ( C is closed & C is boundary ) by TOPS_3:27;
 not C is empty by A1, XBOOLE_1:3;
then consider X1 being non empty strict closed boundary SubSpace of X such that
A3: C = the carrier of X1 by A2, Th67;
take  X1 ; ::_thesis: X0 is SubSpace of X1
thus  X0 is SubSpace of X1 by A1, A3, TSEP_1:4; ::_thesis: verum
end;
given X1 being non empty strict closed boundary SubSpace of X such that A4: X0 is SubSpace of X1 ; ::_thesis: X0 is nowhere_dense
reconsider C = the carrier of X1 as Subset of X by TSEP_1:1;
now__::_thesis:_ex_C_being_Subset_of_X_st_
(_A_c=_C_&_C_is_boundary_&_C_is_closed_)
take C = C; ::_thesis: ( A c= C & C is boundary & C is closed )
thus  ( A c= C & C is boundary & C is closed ) by A4, Def3, TSEP_1:4, TSEP_1:11; ::_thesis: verum
end;
then  for A being Subset of X st A = the carrier of X0 holds
A is nowhere_dense by TOPS_3:27;
hence  X0 is nowhere_dense by Def4; ::_thesis: verum
end;

theorem :: TEX_3:72
for X being non empty non almost_discrete TopSpace
for X0 being non empty nowhere_dense SubSpace of X holds
( ( X0 is boundary & X0 is closed ) or ex X1 being non empty strict proper everywhere_dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st
( X1 meet X2 = TopStruct(# the carrier of X0, the topology of X0 #) & X1 union X2 = TopStruct(# the carrier of X, the topology of X #) ) )
proof
let X be non empty non almost_discrete TopSpace; ::_thesis: for X0 being non empty nowhere_dense SubSpace of X holds
( ( X0 is boundary & X0 is closed ) or ex X1 being non empty strict proper everywhere_dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st
( X1 meet X2 = TopStruct(# the carrier of X0, the topology of X0 #) & X1 union X2 = TopStruct(# the carrier of X, the topology of X #) ) )
let X0 be non empty nowhere_dense SubSpace of X; ::_thesis: ( ( X0 is boundary & X0 is closed ) or ex X1 being non empty strict proper everywhere_dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st
( X1 meet X2 = TopStruct(# the carrier of X0, the topology of X0 #) & X1 union X2 = TopStruct(# the carrier of X, the topology of X #) ) )
reconsider D = the carrier of X0 as non empty Subset of X by TSEP_1:1;
A1: X is SubSpace of X by TSEP_1:2;
 D is nowhere_dense by Th35;
then consider C, B being Subset of X such that
A2: ( C is closed & C is boundary ) and
A3: B is everywhere_dense and
A4: C /\ B = D and
A5: C \/ B = the carrier of X by TOPS_3:51;
 B <> {} by A4;
then consider X1 being non empty strict everywhere_dense SubSpace of X such that
A6: B = the carrier of X1 by A3, Th17;
assume A7: ( not X0 is boundary or not X0 is closed ) ; ::_thesis: ex X1 being non empty strict proper everywhere_dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st
( X1 meet X2 = TopStruct(# the carrier of X0, the topology of X0 #) & X1 union X2 = TopStruct(# the carrier of X, the topology of X #) )
now__::_thesis:_B_is_proper
assume  not B is proper ; ::_thesis: contradiction
then  B = the carrier of X by SUBSET_1:def_6;
then  D = C by A4, XBOOLE_1:28;
hence  contradiction by A7, A2, TSEP_1:11; ::_thesis: verum
end;
then reconsider X1 = X1 as non empty strict proper everywhere_dense SubSpace of X by A6, TEX_2:8;
 C <> {} by A4;
then consider X2 being non empty strict closed boundary SubSpace of X such that
A8: C = the carrier of X2 by A2, Th67;
take  X1 ; ::_thesis: ex X2 being non empty strict closed boundary SubSpace of X st
( X1 meet X2 = TopStruct(# the carrier of X0, the topology of X0 #) & X1 union X2 = TopStruct(# the carrier of X, the topology of X #) )
take  X2 ; ::_thesis: ( X1 meet X2 = TopStruct(# the carrier of X0, the topology of X0 #) & X1 union X2 = TopStruct(# the carrier of X, the topology of X #) )
 C meets B by A4, XBOOLE_0:def_7;
then  X1 meets X2 by A8, A6, TSEP_1:def_3;
then  the carrier of (X1 meet X2) = D by A4, A8, A6, TSEP_1:def_4;
hence  X1 meet X2 = TopStruct(# the carrier of X0, the topology of X0 #) by TSEP_1:5; ::_thesis: X1 union X2 = TopStruct(# the carrier of X, the topology of X #)
 the carrier of (X1 union X2) = the carrier of X by A5, A8, A6, TSEP_1:def_2;
hence  X1 union X2 = TopStruct(# the carrier of X, the topology of X #) by A1, TSEP_1:5; ::_thesis: verum
end;

theorem :: TEX_3:73
for X being non empty non almost_discrete TopSpace
for X0 being non empty everywhere_dense SubSpace of X holds
( ( X0 is dense & X0 is open ) or ex X1 being non empty strict open proper dense SubSpace of X ex X2 being non empty strict nowhere_dense SubSpace of X st
( X1 misses X2 & X1 union X2 = TopStruct(# the carrier of X0, the topology of X0 #) ) )
proof
let X be non empty non almost_discrete TopSpace; ::_thesis: for X0 being non empty everywhere_dense SubSpace of X holds
( ( X0 is dense & X0 is open ) or ex X1 being non empty strict open proper dense SubSpace of X ex X2 being non empty strict nowhere_dense SubSpace of X st
( X1 misses X2 & X1 union X2 = TopStruct(# the carrier of X0, the topology of X0 #) ) )
let X0 be non empty everywhere_dense SubSpace of X; ::_thesis: ( ( X0 is dense & X0 is open ) or ex X1 being non empty strict open proper dense SubSpace of X ex X2 being non empty strict nowhere_dense SubSpace of X st
( X1 misses X2 & X1 union X2 = TopStruct(# the carrier of X0, the topology of X0 #) ) )
reconsider D = the carrier of X0 as non empty Subset of X by TSEP_1:1;
 D is everywhere_dense by Th16;
then consider C, B being Subset of X such that
A1: ( C is open & C is dense ) and
A2: B is nowhere_dense and
A3: C \/ B = D and
A4: C misses B by TOPS_3:49;
 C <> {} by A1, TOPS_3:17;
then consider X1 being non empty strict open dense SubSpace of X such that
A5: C = the carrier of X1 by A1, Th23;
assume A6: ( not X0 is dense or not X0 is open ) ; ::_thesis: ex X1 being non empty strict open proper dense SubSpace of X ex X2 being non empty strict nowhere_dense SubSpace of X st
( X1 misses X2 & X1 union X2 = TopStruct(# the carrier of X0, the topology of X0 #) )
now__::_thesis:_C_is_proper
assume  not C is proper ; ::_thesis: contradiction
then A7: C = the carrier of X by SUBSET_1:def_6;
 C c= D by A3, XBOOLE_1:7;
then  D = [#] X by A7, XBOOLE_0:def_10;
then  ( D is dense & D is open ) ;
hence  contradiction by A6, TSEP_1:16; ::_thesis: verum
end;
then reconsider X1 = X1 as non empty strict open proper dense SubSpace of X by A5, TEX_2:8;
now__::_thesis:_not_B_=_{}
percases ( not X0 is dense or not X0 is open ) by A6;
supposeA8: not X0 is dense ; ::_thesis: not B = {}
assume  B = {} ; ::_thesis: contradiction
thus  contradiction by A8; ::_thesis: verum
end;
supposeA9: not X0 is open ; ::_thesis: not B = {}
assume  B = {} ; ::_thesis: contradiction
hence  contradiction by A1, A3, A9, TSEP_1:16; ::_thesis: verum
end;
end;
end;
then consider X2 being non empty strict nowhere_dense SubSpace of X such that
A10: B = the carrier of X2 by A2, Th62;
take  X1 ; ::_thesis: ex X2 being non empty strict nowhere_dense SubSpace of X st
( X1 misses X2 & X1 union X2 = TopStruct(# the carrier of X0, the topology of X0 #) )
take  X2 ; ::_thesis: ( X1 misses X2 & X1 union X2 = TopStruct(# the carrier of X0, the topology of X0 #) )
thus  X1 misses X2 by A4, A5, A10, TSEP_1:def_3; ::_thesis: X1 union X2 = TopStruct(# the carrier of X0, the topology of X0 #)
 the carrier of (X1 union X2) = the carrier of X0 by A3, A5, A10, TSEP_1:def_2;
hence  X1 union X2 = TopStruct(# the carrier of X0, the topology of X0 #) by TSEP_1:5; ::_thesis: verum
end;

theorem :: TEX_3:74
for X being non empty non almost_discrete TopSpace
for X0 being non empty nowhere_dense SubSpace of X ex X1 being non empty strict open proper dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st
( X1,X2 constitute_a_decomposition & X0 is SubSpace of X2 )
proof
let X be non empty non almost_discrete TopSpace; ::_thesis: for X0 being non empty nowhere_dense SubSpace of X ex X1 being non empty strict open proper dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st
( X1,X2 constitute_a_decomposition & X0 is SubSpace of X2 )
let X0 be non empty nowhere_dense SubSpace of X; ::_thesis: ex X1 being non empty strict open proper dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st
( X1,X2 constitute_a_decomposition & X0 is SubSpace of X2 )
reconsider D = the carrier of X0 as non empty Subset of X by TSEP_1:1;
 D is nowhere_dense by Th35;
then consider C, B being Subset of X such that
A1: ( C is closed & C is boundary ) and
A2: ( B is open & B is dense ) and
A3: C /\ (D \/ B) = D and
A4: C misses B and
A5: C \/ B = the carrier of X by TOPS_3:52;
 B <> {} by A2, TOPS_3:17;
then consider X1 being non empty strict open dense SubSpace of X such that
A6: B = the carrier of X1 by A2, Th23;
A7: C <> {} by A3;
then consider X2 being non empty strict closed boundary SubSpace of X such that
A8: C = the carrier of X2 by A1, Th67;
A9: C /\ B = {} by A4, XBOOLE_0:def_7;
now__::_thesis:_B_is_proper
assume  not B is proper ; ::_thesis: contradiction
then  B = the carrier of X by SUBSET_1:def_6;
hence  contradiction by A7, A9, XBOOLE_1:28; ::_thesis: verum
end;
then reconsider X1 = X1 as non empty strict open proper dense SubSpace of X by A6, TEX_2:8;
take  X1 ; ::_thesis: ex X2 being non empty strict closed boundary SubSpace of X st
( X1,X2 constitute_a_decomposition & X0 is SubSpace of X2 )
take  X2 ; ::_thesis: ( X1,X2 constitute_a_decomposition & X0 is SubSpace of X2 )
 for P, Q being Subset of X st P = the carrier of X1 & Q = the carrier of X2 holds
P,Q constitute_a_decomposition by A4, A5, A6, A8, TSEP_2:def_1;
hence  X1,X2 constitute_a_decomposition by TSEP_2:def_2; ::_thesis: X0 is SubSpace of X2
 D c= C by A3, XBOOLE_1:17;
hence  X0 is SubSpace of X2 by A8, TSEP_1:4; ::_thesis: verum
end;

theorem :: TEX_3:75
for X being non empty non almost_discrete TopSpace
for X0 being proper everywhere_dense SubSpace of X ex X1 being strict open proper dense SubSpace of X ex X2 being strict closed boundary SubSpace of X st
( X1,X2 constitute_a_decomposition & X1 is SubSpace of X0 )
proof
let X be non empty non almost_discrete TopSpace; ::_thesis: for X0 being proper everywhere_dense SubSpace of X ex X1 being strict open proper dense SubSpace of X ex X2 being strict closed boundary SubSpace of X st
( X1,X2 constitute_a_decomposition & X1 is SubSpace of X0 )
let X0 be proper everywhere_dense SubSpace of X; ::_thesis: ex X1 being strict open proper dense SubSpace of X ex X2 being strict closed boundary SubSpace of X st
( X1,X2 constitute_a_decomposition & X1 is SubSpace of X0 )
reconsider D = the carrier of X0 as Subset of X by TSEP_1:1;
 D is everywhere_dense by Th16;
then consider C, B being Subset of X such that
A1: ( C is open & C is dense ) and
A2: ( B is closed & B is boundary ) and
A3: C \/ (D /\ B) = D and
A4: C misses B and
A5: C \/ B = the carrier of X by TOPS_3:50;
 C <> {} by A1, TOPS_3:17;
then consider X1 being non empty strict open dense SubSpace of X such that
A6: C = the carrier of X1 by A1, Th23;
A7: now__::_thesis:_C_is_proper
assume  not C is proper ; ::_thesis: contradiction
then  C = the carrier of X by SUBSET_1:def_6;
then  the carrier of X c= D by A3, XBOOLE_1:7;
then  D = the carrier of X by XBOOLE_0:def_10;
then  not D is proper by SUBSET_1:def_6;
hence  contradiction by TEX_2:8; ::_thesis: verum
end;
then  not B is empty by A5, SUBSET_1:def_6;
then consider X2 being non empty strict closed boundary SubSpace of X such that
A8: B = the carrier of X2 by A2, Th67;
reconsider X1 = X1 as strict open proper dense SubSpace of X by A6, A7, TEX_2:8;
take  X1 ; ::_thesis: ex X2 being strict closed boundary SubSpace of X st
( X1,X2 constitute_a_decomposition & X1 is SubSpace of X0 )
take  X2 ; ::_thesis: ( X1,X2 constitute_a_decomposition & X1 is SubSpace of X0 )
 for P, Q being Subset of X st P = the carrier of X1 & Q = the carrier of X2 holds
P,Q constitute_a_decomposition by A4, A5, A6, A8, TSEP_2:def_1;
hence  X1,X2 constitute_a_decomposition by TSEP_2:def_2; ::_thesis: X1 is SubSpace of X0
 C c= D by A3, XBOOLE_1:7;
hence  X1 is SubSpace of X0 by A6, TSEP_1:4; ::_thesis: verum
end;