:: TOPS_3 semantic presentation

begin


theorem Th1: :: TOPS_3:1
for X being TopStruct
for A being Subset of X holds
( ( A = {} X implies A ` = [#] X ) & ( A ` = [#] X implies A = {} X ) & ( A = {} implies A ` = the carrier of X ) & ( A ` = the carrier of X implies A = {} ) )
proof
let X be TopStruct ; ::_thesis: for A being Subset of X holds
( ( A = {} X implies A ` = [#] X ) & ( A ` = [#] X implies A = {} X ) & ( A = {} implies A ` = the carrier of X ) & ( A ` = the carrier of X implies A = {} ) )
let A be Subset of X; ::_thesis: ( ( A = {} X implies A ` = [#] X ) & ( A ` = [#] X implies A = {} X ) & ( A = {} implies A ` = the carrier of X ) & ( A ` = the carrier of X implies A = {} ) )
thus  ( A = {} X iff A ` = [#] X ) ::_thesis: ( A = {} iff A ` = the carrier of X )
proof
thus  ( A = {} X implies A ` = [#] X ) ; ::_thesis: ( A ` = [#] X implies A = {} X )
assume  A ` = [#] X ; ::_thesis: A = {} X
then  (A `) ` = {} X by XBOOLE_1:37;
hence  A = {} X ; ::_thesis: verum
end;
hence  ( A = {} iff A ` = the carrier of X ) ; ::_thesis: verum
end;

theorem Th2: :: TOPS_3:2
for X being TopStruct
for A being Subset of X holds
( ( A = [#] X implies A ` = {} X ) & ( A ` = {} X implies A = [#] X ) & ( A = the carrier of X implies A ` = {} ) & ( A ` = {} implies A = the carrier of X ) )
proof
let X be TopStruct ; ::_thesis: for A being Subset of X holds
( ( A = [#] X implies A ` = {} X ) & ( A ` = {} X implies A = [#] X ) & ( A = the carrier of X implies A ` = {} ) & ( A ` = {} implies A = the carrier of X ) )
let A be Subset of X; ::_thesis: ( ( A = [#] X implies A ` = {} X ) & ( A ` = {} X implies A = [#] X ) & ( A = the carrier of X implies A ` = {} ) & ( A ` = {} implies A = the carrier of X ) )
thus  ( A = [#] X iff A ` = {} X ) ::_thesis: ( A = the carrier of X iff A ` = {} )
proof
thus  ( A = [#] X implies A ` = {} X ) by XBOOLE_1:37; ::_thesis: ( A ` = {} X implies A = [#] X )
assume  A ` = {} X ; ::_thesis: A = [#] X
then  (A `) ` = [#] X ;
hence  A = [#] X ; ::_thesis: verum
end;
hence  ( A = the carrier of X iff A ` = {} ) ; ::_thesis: verum
end;

theorem Th3: :: TOPS_3:3
for X being TopSpace
for A, B being Subset of X holds (Int A) /\ (Cl B) c= Cl (A /\ B)
proof
let X be TopSpace; ::_thesis: for A, B being Subset of X holds (Int A) /\ (Cl B) c= Cl (A /\ B)
let A, B be Subset of X; ::_thesis: (Int A) /\ (Cl B) c= Cl (A /\ B)
 (Int A) /\ B c= A /\ B by TOPS_1:16, XBOOLE_1:26;
then A1: Cl ((Int A) /\ B) c= Cl (A /\ B) by PRE_TOPC:19;
 (Int A) /\ (Cl B) c= Cl ((Int A) /\ B) by TOPS_1:13;
hence  (Int A) /\ (Cl B) c= Cl (A /\ B) by A1, XBOOLE_1:1; ::_thesis: verum
end;


theorem Th4: :: TOPS_3:4
for X being TopSpace
for A, B being Subset of X holds Int (A \/ B) c= (Cl A) \/ (Int B)
proof
let X be TopSpace; ::_thesis: for A, B being Subset of X holds Int (A \/ B) c= (Cl A) \/ (Int B)
let A, B be Subset of X; ::_thesis: Int (A \/ B) c= (Cl A) \/ (Int B)
 (Int (A `)) /\ (Cl (B `)) c= Cl ((A `) /\ (B `)) by Th3;
then  (Cl ((A `) /\ (B `))) ` c= ((Int (A `)) /\ (Cl (B `))) ` by SUBSET_1:12;
then  Int (((A `) /\ (B `)) `) c= ((Int (A `)) /\ (Cl (B `))) ` by TDLAT_3:3;
then  Int (((A `) `) \/ ((B `) `)) c= ((Int (A `)) /\ (Cl (B `))) ` by XBOOLE_1:54;
then  Int (A \/ B) c= ((Int (A `)) `) \/ ((Cl (B `)) `) by XBOOLE_1:54;
then  Int (A \/ B) c= (Cl A) \/ ((Cl (B `)) `) by TDLAT_3:1;
hence  Int (A \/ B) c= (Cl A) \/ (Int B) by TOPS_1:def_1; ::_thesis: verum
end;

theorem Th5: :: TOPS_3:5
for X being TopSpace
for B, A being Subset of X st A is closed holds
Int (A \/ B) c= A \/ (Int B)
proof
let X be TopSpace; ::_thesis: for B, A being Subset of X st A is closed holds
Int (A \/ B) c= A \/ (Int B)
let B, A be Subset of X; ::_thesis: ( A is closed implies Int (A \/ B) c= A \/ (Int B) )
assume  A is closed ; ::_thesis: Int (A \/ B) c= A \/ (Int B)
then  Cl A = A by PRE_TOPC:22;
hence  Int (A \/ B) c= A \/ (Int B) by Th4; ::_thesis: verum
end;

theorem Th6: :: TOPS_3:6
for X being TopSpace
for B, A being Subset of X st A is closed holds
Int (A \/ B) = Int (A \/ (Int B))
proof
let X be TopSpace; ::_thesis: for B, A being Subset of X st A is closed holds
Int (A \/ B) = Int (A \/ (Int B))
let B, A be Subset of X; ::_thesis: ( A is closed implies Int (A \/ B) = Int (A \/ (Int B)) )
 A \/ (Int B) c= A \/ B by TOPS_1:16, XBOOLE_1:9;
then A1: Int (A \/ (Int B)) c= Int (A \/ B) by TOPS_1:19;
assume  A is closed ; ::_thesis: Int (A \/ B) = Int (A \/ (Int B))
then  Int (Int (A \/ B)) c= Int (A \/ (Int B)) by Th5, TOPS_1:19;
hence  Int (A \/ B) = Int (A \/ (Int B)) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th7: :: TOPS_3:7
for X being TopSpace
for A being Subset of X st A misses Int (Cl A) holds
Int (Cl A) = {}
proof
let X be TopSpace; ::_thesis: for A being Subset of X st A misses Int (Cl A) holds
Int (Cl A) = {}
let A be Subset of X; ::_thesis: ( A misses Int (Cl A) implies Int (Cl A) = {} )
reconsider A9 = A as Subset of X ;
assume  A /\ (Int (Cl A)) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: Int (Cl A) = {}
then  A9 misses Int (Cl A9) by XBOOLE_0:def_7;
then  Cl A misses Int (Cl A) by TSEP_1:36;
then  (Cl A) /\ (Int (Cl A)) = {} by XBOOLE_0:def_7;
hence  Int (Cl A) = {} by TOPS_1:16, XBOOLE_1:28; ::_thesis: verum
end;

theorem :: TOPS_3:8
for X being TopSpace
for A being Subset of X st A \/ (Cl (Int A)) = the carrier of X holds
Cl (Int A) = the carrier of X
proof
let X be TopSpace; ::_thesis: for A being Subset of X st A \/ (Cl (Int A)) = the carrier of X holds
Cl (Int A) = the carrier of X
let A be Subset of X; ::_thesis: ( A \/ (Cl (Int A)) = the carrier of X implies Cl (Int A) = the carrier of X )
assume  A \/ (Cl (Int A)) = the carrier of X ; ::_thesis: Cl (Int A) = the carrier of X
then  (Int A) \/ (Cl (Int A)) = the carrier of X by TDLAT_3:4;
hence  Cl (Int A) = the carrier of X by PRE_TOPC:18, XBOOLE_1:12; ::_thesis: verum
end;

begin

definition
let X be TopStruct ;
let A be Subset of X;
redefine attr A is boundary  means :Def1: :: TOPS_3:def 1
 Int A = {} ;
compatibility
 ( A is boundary iff Int A = {} ) by TOPS_1:48;
end;

:: deftheorem Def1 defines boundary TOPS_3:def_1_:_
 for X being TopStruct
for A being Subset of X holds
( A is boundary iff Int A = {} );

theorem :: TOPS_3:9
for X being TopSpace holds {} X is boundary ;


theorem Th10: :: TOPS_3:10
for X being non empty TopSpace
for A being Subset of X st A is boundary holds
A <> the carrier of X
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X st A is boundary holds
A <> the carrier of X
let A be Subset of X; ::_thesis: ( A is boundary implies A <> the carrier of X )
assume A1: Int A = {} ; :: according to TOPS_3:def_1 ::_thesis: A <> the carrier of X
assume  A = the carrier of X ; ::_thesis: contradiction
then  A = [#] X ;
hence  contradiction by A1, TOPS_1:15; ::_thesis: verum
end;


theorem Th11: :: TOPS_3:11
for X being TopSpace
for B, A being Subset of X st B is boundary & A c= B holds
A is boundary
proof
let X be TopSpace; ::_thesis: for B, A being Subset of X st B is boundary & A c= B holds
A is boundary
let B, A be Subset of X; ::_thesis: ( B is boundary & A c= B implies A is boundary )
assume  B is boundary ; ::_thesis: ( not A c= B or A is boundary )
then A1: Int B = {} ;
assume  A c= B ; ::_thesis: A is boundary
then  Int A = {} by A1, TOPS_1:19, XBOOLE_1:3;
hence  A is boundary by TOPS_1:48; ::_thesis: verum
end;

theorem :: TOPS_3:12
for X being TopSpace
for A being Subset of X holds
( A is boundary iff for C being Subset of X st A ` c= C & C is closed holds
C = the carrier of X )
proof
let X be TopSpace; ::_thesis: for A being Subset of X holds
( A is boundary iff for C being Subset of X st A ` c= C & C is closed holds
C = the carrier of X )
let A be Subset of X; ::_thesis: ( A is boundary iff for C being Subset of X st A ` c= C & C is closed holds
C = the carrier of X )
thus  ( A is boundary implies for C being Subset of X st A ` c= C & C is closed holds
C = the carrier of X ) ::_thesis: ( ( for C being Subset of X st A ` c= C & C is closed holds
C = the carrier of X ) implies A is boundary )
proof
assume A1: A is boundary ; ::_thesis: for C being Subset of X st A ` c= C & C is closed holds
C = the carrier of X
let C be Subset of X; ::_thesis: ( A ` c= C & C is closed implies C = the carrier of X )
assume  A ` c= C ; ::_thesis: ( not C is closed or C = the carrier of X )
then A2: C ` c= (A `) ` by SUBSET_1:12;
assume  C is closed ; ::_thesis: C = the carrier of X
then  C ` = {} X by A1, A2, TOPS_1:50;
hence  C = the carrier of X by Th2; ::_thesis: verum
end;
assume A3: for C being Subset of X st A ` c= C & C is closed holds
C = the carrier of X ; ::_thesis: A is boundary
now__::_thesis:_for_G_being_Subset_of_X_st_G_c=_A_&_G_is_open_holds_
G_=_{}
let G be Subset of X; ::_thesis: ( G c= A & G is open implies G = {} )
assume that
A4: G c= A and
A5: G is open ; ::_thesis: G = {}
 A ` c= G ` by A4, SUBSET_1:12;
then  G ` = the carrier of X by A3, A5;
hence  G = {} by Th1; ::_thesis: verum
end;
hence  A is boundary by TOPS_1:50; ::_thesis: verum
end;

theorem :: TOPS_3:13
for X being TopSpace
for A being Subset of X holds
( A is boundary iff for G being Subset of X st G <> {} & G is open holds
A ` meets G )
proof
let X be TopSpace; ::_thesis: for A being Subset of X holds
( A is boundary iff for G being Subset of X st G <> {} & G is open holds
A ` meets G )
let A be Subset of X; ::_thesis: ( A is boundary iff for G being Subset of X st G <> {} & G is open holds
A ` meets G )
thus  ( A is boundary implies for G being Subset of X st G <> {} & G is open holds
A ` meets G ) ::_thesis: ( ( for G being Subset of X st G <> {} & G is open holds
A ` meets G ) implies A is boundary )
proof
assume A1: A is boundary ; ::_thesis: for G being Subset of X st G <> {} & G is open holds
A ` meets G
let G be Subset of X; ::_thesis: ( G <> {} & G is open implies A ` meets G )
assume A2: G <> {} ; ::_thesis: ( not G is open or A ` meets G )
assume A3: G is open ; ::_thesis: A ` meets G
assume  A ` misses G ; ::_thesis: contradiction
then  G c= A by SUBSET_1:24;
hence  contradiction by A1, A2, A3, TOPS_1:50; ::_thesis: verum
end;
assume A4: for G being Subset of X st G <> {} & G is open holds
A ` meets G ; ::_thesis: A is boundary
assume  Int A <> {} ; :: according to TOPS_3:def_1 ::_thesis: contradiction
then  ( Int A c= A & A ` meets Int A ) by A4, TOPS_1:16;
hence  contradiction by SUBSET_1:24; ::_thesis: verum
end;

theorem :: TOPS_3:14
for X being TopSpace
for A being Subset of X holds
( A is boundary iff for F being Subset of X st F is closed holds
Int F = Int (F \/ A) )
proof
let X be TopSpace; ::_thesis: for A being Subset of X holds
( A is boundary iff for F being Subset of X st F is closed holds
Int F = Int (F \/ A) )
let A be Subset of X; ::_thesis: ( A is boundary iff for F being Subset of X st F is closed holds
Int F = Int (F \/ A) )
thus  ( A is boundary implies for F being Subset of X st F is closed holds
Int F = Int (F \/ A) ) ::_thesis: ( ( for F being Subset of X st F is closed holds
Int F = Int (F \/ A) ) implies A is boundary )
proof
assume A1: Int A = {} ; :: according to TOPS_3:def_1 ::_thesis: for F being Subset of X st F is closed holds
Int F = Int (F \/ A)
let F be Subset of X; ::_thesis: ( F is closed implies Int F = Int (F \/ A) )
assume  F is closed ; ::_thesis: Int F = Int (F \/ A)
then  Int (F \/ A) = Int (F \/ (Int A)) by Th6;
hence  Int F = Int (F \/ A) by A1; ::_thesis: verum
end;
assume  for F being Subset of X st F is closed holds
Int F = Int (F \/ A) ; ::_thesis: A is boundary
then  Int ({} X) = Int (({} X) \/ A) ;
hence  A is boundary by Def1; ::_thesis: verum
end;

theorem :: TOPS_3:15
for X being TopSpace
for A, B being Subset of X st A is boundary holds
A /\ B is boundary by Th11, XBOOLE_1:17;

definition
let X be TopStruct ;
let A be Subset of X;
redefine attr A is dense  means :Def2: :: TOPS_3:def 2
 Cl A = the carrier of X;
compatibility
 ( A is dense iff Cl A = the carrier of X )
proof
thus  ( A is dense implies Cl A = the carrier of X ) ::_thesis: ( Cl A = the carrier of X implies A is dense )
proof
assume  A is dense ; ::_thesis: Cl A = the carrier of X
then  Cl A = [#] X by TOPS_1:def_3;
hence  Cl A = the carrier of X ; ::_thesis: verum
end;
assume  Cl A = the carrier of X ; ::_thesis: A is dense
then  Cl A = [#] X ;
hence  A is dense by TOPS_1:def_3; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines dense TOPS_3:def_2_:_
 for X being TopStruct
for A being Subset of X holds
( A is dense iff Cl A = the carrier of X );

theorem :: TOPS_3:16
for X being TopSpace holds [#] X is dense ;


theorem Th17: :: TOPS_3:17
for X being non empty TopSpace
for A being Subset of X st A is dense holds
A <> {}
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X st A is dense holds
A <> {}
let A be Subset of X; ::_thesis: ( A is dense implies A <> {} )
assume  A is dense ; ::_thesis: A <> {}
then A1: Cl A = [#] X by TOPS_1:def_3;
assume  A = {} ; ::_thesis: contradiction
hence  contradiction by A1, PRE_TOPC:22; ::_thesis: verum
end;

theorem Th18: :: TOPS_3:18
for X being non empty TopSpace
for A being Subset of X holds
( A is dense iff A ` is boundary )
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X holds
( A is dense iff A ` is boundary )
let A be Subset of X; ::_thesis: ( A is dense iff A ` is boundary )
thus  ( A is dense implies A ` is boundary ) ::_thesis: ( A ` is boundary implies A is dense )
proof
assume  A is dense ; ::_thesis: A ` is boundary
then  (A `) ` is dense ;
hence  A ` is boundary by TOPS_1:def_4; ::_thesis: verum
end;
assume  A ` is boundary ; ::_thesis: A is dense
then  (A `) ` is dense by TOPS_1:def_4;
hence  A is dense ; ::_thesis: verum
end;

theorem :: TOPS_3:19
for X being non empty TopSpace
for A being Subset of X holds
( A is dense iff for C being Subset of X st A c= C & C is closed holds
C = the carrier of X )
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X holds
( A is dense iff for C being Subset of X st A c= C & C is closed holds
C = the carrier of X )
let A be Subset of X; ::_thesis: ( A is dense iff for C being Subset of X st A c= C & C is closed holds
C = the carrier of X )
thus  ( A is dense implies for C being Subset of X st A c= C & C is closed holds
C = the carrier of X ) ::_thesis: ( ( for C being Subset of X st A c= C & C is closed holds
C = the carrier of X ) implies A is dense )
proof
assume A1: Cl A = the carrier of X ; :: according to TOPS_3:def_2 ::_thesis: for C being Subset of X st A c= C & C is closed holds
C = the carrier of X
let C be Subset of X; ::_thesis: ( A c= C & C is closed implies C = the carrier of X )
assume  ( A c= C & C is closed ) ; ::_thesis: C = the carrier of X
then  Cl A c= C by TOPS_1:5;
hence  C = the carrier of X by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
assume  for C being Subset of X st A c= C & C is closed holds
C = the carrier of X ; ::_thesis: A is dense
then  Cl A = the carrier of X by PRE_TOPC:18;
hence  A is dense by Def2; ::_thesis: verum
end;

theorem :: TOPS_3:20
for X being non empty TopSpace
for A being Subset of X holds
( A is dense iff for G being Subset of X st G is open holds
Cl G = Cl (G /\ A) )
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X holds
( A is dense iff for G being Subset of X st G is open holds
Cl G = Cl (G /\ A) )
let A be Subset of X; ::_thesis: ( A is dense iff for G being Subset of X st G is open holds
Cl G = Cl (G /\ A) )
thus  ( A is dense implies for G being Subset of X st G is open holds
Cl G = Cl (G /\ A) ) ::_thesis: ( ( for G being Subset of X st G is open holds
Cl G = Cl (G /\ A) ) implies A is dense )
proof
assume A1: A is dense ; ::_thesis: for G being Subset of X st G is open holds
Cl G = Cl (G /\ A)
let G be Subset of X; ::_thesis: ( G is open implies Cl G = Cl (G /\ A) )
assume  G is open ; ::_thesis: Cl G = Cl (G /\ A)
then A2: Cl (G /\ (Cl A)) = Cl (G /\ A) by TOPS_1:14;
 G /\ ([#] X) = G by XBOOLE_1:28;
hence  Cl G = Cl (G /\ A) by A1, A2, TOPS_1:def_3; ::_thesis: verum
end;
assume  for G being Subset of X st G is open holds
Cl G = Cl (G /\ A) ; ::_thesis: A is dense
then  Cl ([#] X) = Cl (([#] X) /\ A) ;
then A3: [#] X = Cl (([#] X) /\ A) by TOPS_1:2;
 ([#] X) /\ A = A by XBOOLE_1:28;
hence  A is dense by A3, Def2; ::_thesis: verum
end;

theorem :: TOPS_3:21
for X being non empty TopSpace
for A, B being Subset of X st A is dense holds
A \/ B is dense by TOPS_1:44, XBOOLE_1:7;

definition
let X be TopStruct ;
let A be Subset of X;
redefine attr A is nowhere_dense  means :Def3: :: TOPS_3:def 3
 Int (Cl A) = {} ;
compatibility
 ( A is nowhere_dense iff Int (Cl A) = {} )
proof
thus  ( A is nowhere_dense implies Int (Cl A) = {} ) ::_thesis: ( Int (Cl A) = {} implies A is nowhere_dense )
proof
assume  A is nowhere_dense ; ::_thesis: Int (Cl A) = {}
then  Cl A is boundary by TOPS_1:def_5;
hence  Int (Cl A) = {} ; ::_thesis: verum
end;
assume  Int (Cl A) = {} ; ::_thesis: A is nowhere_dense
then  Cl A is boundary by Def1;
hence  A is nowhere_dense by TOPS_1:def_5; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines nowhere_dense TOPS_3:def_3_:_
 for X being TopStruct
for A being Subset of X holds
( A is nowhere_dense iff Int (Cl A) = {} );

theorem :: TOPS_3:22
for X being non empty TopSpace holds {} X is nowhere_dense ;

theorem :: TOPS_3:23
for X being non empty TopSpace
for A being Subset of X st A is nowhere_dense holds
A <> the carrier of X by Th10;

theorem :: TOPS_3:24
for X being non empty TopSpace
for A being Subset of X st A is nowhere_dense holds
Cl A is nowhere_dense
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X st A is nowhere_dense holds
Cl A is nowhere_dense
let A be Subset of X; ::_thesis: ( A is nowhere_dense implies Cl A is nowhere_dense )
assume  A is nowhere_dense ; ::_thesis: Cl A is nowhere_dense
then  Cl A is boundary by TOPS_1:def_5;
hence  Cl A is nowhere_dense ; ::_thesis: verum
end;

theorem :: TOPS_3:25
for X being non empty TopSpace
for A being Subset of X st A is nowhere_dense holds
not A is dense
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X st A is nowhere_dense holds
not A is dense
let A be Subset of X; ::_thesis: ( A is nowhere_dense implies not A is dense )
assume A1: Int (Cl A) = {} ; :: according to TOPS_3:def_3 ::_thesis: not A is dense
assume  A is dense ; ::_thesis: contradiction
then  Cl A = [#] X by TOPS_1:def_3;
hence  contradiction by A1, TOPS_1:15; ::_thesis: verum
end;

theorem Th26: :: TOPS_3:26
for X being non empty TopSpace
for B, A being Subset of X st B is nowhere_dense & A c= B holds
A is nowhere_dense
proof
let X be non empty TopSpace; ::_thesis: for B, A being Subset of X st B is nowhere_dense & A c= B holds
A is nowhere_dense
let B, A be Subset of X; ::_thesis: ( B is nowhere_dense & A c= B implies A is nowhere_dense )
assume  B is nowhere_dense ; ::_thesis: ( not A c= B or A is nowhere_dense )
then A1: Cl B is boundary by TOPS_1:def_5;
assume  A c= B ; ::_thesis: A is nowhere_dense
then  Cl A is boundary by A1, Th11, PRE_TOPC:19;
hence  A is nowhere_dense by TOPS_1:def_5; ::_thesis: verum
end;

theorem Th27: :: TOPS_3:27
for X being non empty TopSpace
for A being Subset of X holds
( A is nowhere_dense iff ex C being Subset of X st
( A c= C & C is closed & C is boundary ) )
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X holds
( A is nowhere_dense iff ex C being Subset of X st
( A c= C & C is closed & C is boundary ) )
let A be Subset of X; ::_thesis: ( A is nowhere_dense iff ex C being Subset of X st
( A c= C & C is closed & C is boundary ) )
thus  ( A is nowhere_dense implies ex C being Subset of X st
( A c= C & C is closed & C is boundary ) ) ::_thesis: ( ex C being Subset of X st
( A c= C & C is closed & C is boundary ) implies A is nowhere_dense )
proof
assume A1: A is nowhere_dense ; ::_thesis: ex C being Subset of X st
( A c= C & C is closed & C is boundary )
take  Cl A ; ::_thesis: ( A c= Cl A & Cl A is closed & Cl A is boundary )
thus  ( A c= Cl A & Cl A is closed & Cl A is boundary ) by A1, PRE_TOPC:18, TOPS_1:def_5; ::_thesis: verum
end;
given C being Subset of X such that A2: ( A c= C & C is closed & C is boundary ) ; ::_thesis: A is nowhere_dense
 Cl A is boundary by A2, Th11, TOPS_1:5;
hence  A is nowhere_dense by TOPS_1:def_5; ::_thesis: verum
end;

theorem Th28: :: TOPS_3:28
for X being non empty TopSpace
for A being Subset of X holds
( A is nowhere_dense iff for G being Subset of X st G <> {} & G is open holds
ex H being Subset of X st
( H c= G & H <> {} & H is open & A misses H ) )
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X holds
( A is nowhere_dense iff for G being Subset of X st G <> {} & G is open holds
ex H being Subset of X st
( H c= G & H <> {} & H is open & A misses H ) )
let A be Subset of X; ::_thesis: ( A is nowhere_dense iff for G being Subset of X st G <> {} & G is open holds
ex H being Subset of X st
( H c= G & H <> {} & H is open & A misses H ) )
thus  ( A is nowhere_dense implies for G being Subset of X st G <> {} & G is open holds
ex H being Subset of X st
( H c= G & H <> {} & H is open & A misses H ) ) ::_thesis: ( ( for G being Subset of X st G <> {} & G is open holds
ex H being Subset of X st
( H c= G & H <> {} & H is open & A misses H ) ) implies A is nowhere_dense )
proof
assume  A is nowhere_dense ; ::_thesis: for G being Subset of X st G <> {} & G is open holds
ex H being Subset of X st
( H c= G & H <> {} & H is open & A misses H )
then A1: Cl A is boundary by TOPS_1:def_5;
let G be Subset of X; ::_thesis: ( G <> {} & G is open implies ex H being Subset of X st
( H c= G & H <> {} & H is open & A misses H ) )
assume  ( G <> {} & G is open ) ; ::_thesis: ex H being Subset of X st
( H c= G & H <> {} & H is open & A misses H )
then consider H being Subset of X such that
A2: ( H c= G & H <> {} & H is open & Cl A misses H ) by A1, TOPS_1:51;
take  H ; ::_thesis: ( H c= G & H <> {} & H is open & A misses H )
thus  ( H c= G & H <> {} & H is open & A misses H ) by A2, PRE_TOPC:18, XBOOLE_1:63; ::_thesis: verum
end;
assume A3: for G being Subset of X st G <> {} & G is open holds
ex H being Subset of X st
( H c= G & H <> {} & H is open & A misses H ) ; ::_thesis: A is nowhere_dense
 for G being Subset of X st G <> {} & G is open holds
ex H being Subset of X st
( H c= G & H <> {} & H is open & Cl A misses H )
proof
let G be Subset of X; ::_thesis: ( G <> {} & G is open implies ex H being Subset of X st
( H c= G & H <> {} & H is open & Cl A misses H ) )
assume  ( G <> {} & G is open ) ; ::_thesis: ex H being Subset of X st
( H c= G & H <> {} & H is open & Cl A misses H )
then consider H being Subset of X such that
A4: ( H c= G & H <> {} & H is open & A misses H ) by A3;
take  H ; ::_thesis: ( H c= G & H <> {} & H is open & Cl A misses H )
thus  ( H c= G & H <> {} & H is open & Cl A misses H ) by A4, TSEP_1:36; ::_thesis: verum
end;
then  Cl A is boundary by TOPS_1:51;
hence  A is nowhere_dense by TOPS_1:def_5; ::_thesis: verum
end;

theorem :: TOPS_3:29
for X being non empty TopSpace
for A, B being Subset of X st A is nowhere_dense holds
A /\ B is nowhere_dense by Th26, XBOOLE_1:17;

theorem Th30: :: TOPS_3:30
for X being non empty TopSpace
for A, B being Subset of X st A is nowhere_dense & B is boundary holds
A \/ B is boundary
proof
let X be non empty TopSpace; ::_thesis: for A, B being Subset of X st A is nowhere_dense & B is boundary holds
A \/ B is boundary
let A, B be Subset of X; ::_thesis: ( A is nowhere_dense & B is boundary implies A \/ B is boundary )
assume  A is nowhere_dense ; ::_thesis: ( not B is boundary or A \/ B is boundary )
then A1: Cl A is boundary by TOPS_1:def_5;
assume  B is boundary ; ::_thesis: A \/ B is boundary
then  ( A c= Cl A & B \/ (Cl A) is boundary ) by A1, PRE_TOPC:18, TOPS_1:49;
hence  A \/ B is boundary by Th11, XBOOLE_1:9; ::_thesis: verum
end;

definition
let X be TopStruct ;
let A be Subset of X;
attrA is everywhere_dense  means :Def4: :: TOPS_3:def 4
 Cl (Int A) = [#] X;
end;

:: deftheorem Def4 defines everywhere_dense TOPS_3:def_4_:_
 for X being TopStruct
for A being Subset of X holds
( A is everywhere_dense iff Cl (Int A) = [#] X );

definition
let X be TopStruct ;
let A be Subset of X;
redefine attr A is everywhere_dense  means :: TOPS_3:def 5
 Cl (Int A) = the carrier of X;
compatibility
 ( A is everywhere_dense iff Cl (Int A) = the carrier of X )
proof
thus  ( A is everywhere_dense implies Cl (Int A) = the carrier of X ) ::_thesis: ( Cl (Int A) = the carrier of X implies A is everywhere_dense )
proof
assume  A is everywhere_dense ; ::_thesis: Cl (Int A) = the carrier of X
then  Cl (Int A) = [#] X by Def4;
hence  Cl (Int A) = the carrier of X ; ::_thesis: verum
end;
assume  Cl (Int A) = the carrier of X ; ::_thesis: A is everywhere_dense
then  Cl (Int A) = [#] X ;
hence  A is everywhere_dense by Def4; ::_thesis: verum
end;
end;

:: deftheorem  defines everywhere_dense TOPS_3:def_5_:_
 for X being TopStruct
for A being Subset of X holds
( A is everywhere_dense iff Cl (Int A) = the carrier of X );

theorem :: TOPS_3:31
for X being non empty TopSpace holds [#] X is everywhere_dense
proof
let X be non empty TopSpace; ::_thesis: [#] X is everywhere_dense
 Int ([#] X) = [#] X by TOPS_1:15;
then  Cl (Int ([#] X)) = [#] X by TOPS_1:2;
hence  [#] X is everywhere_dense by Def4; ::_thesis: verum
end;

theorem Th32: :: TOPS_3:32
for X being non empty TopSpace
for A being Subset of X st A is everywhere_dense holds
Int A is everywhere_dense
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X st A is everywhere_dense holds
Int A is everywhere_dense
let A be Subset of X; ::_thesis: ( A is everywhere_dense implies Int A is everywhere_dense )
assume  A is everywhere_dense ; ::_thesis: Int A is everywhere_dense
then  Cl (Int (Int A)) = [#] X by Def4;
hence  Int A is everywhere_dense by Def4; ::_thesis: verum
end;

theorem Th33: :: TOPS_3:33
for X being non empty TopSpace
for A being Subset of X st A is everywhere_dense holds
A is dense
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X st A is everywhere_dense holds
A is dense
let A be Subset of X; ::_thesis: ( A is everywhere_dense implies A is dense )
assume  A is everywhere_dense ; ::_thesis: A is dense
then  Cl (Int A) = [#] X by Def4;
then  [#] X c= Cl A by PRE_TOPC:19, TOPS_1:16;
then  Cl A = [#] X by XBOOLE_0:def_10;
hence  A is dense by TOPS_1:def_3; ::_thesis: verum
end;

theorem :: TOPS_3:34
for X being non empty TopSpace
for A being Subset of X st A is everywhere_dense holds
A <> {} by Th17, Th33;

theorem Th35: :: TOPS_3:35
for X being non empty TopSpace
for A being Subset of X holds
( A is everywhere_dense iff Int A is dense )
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X holds
( A is everywhere_dense iff Int A is dense )
let A be Subset of X; ::_thesis: ( A is everywhere_dense iff Int A is dense )
thus  ( A is everywhere_dense implies Int A is dense ) by Th32, Th33; ::_thesis: ( Int A is dense implies A is everywhere_dense )
assume  Int A is dense ; ::_thesis: A is everywhere_dense
then  Cl (Int A) = [#] X by TOPS_1:def_3;
hence  A is everywhere_dense by Def4; ::_thesis: verum
end;

theorem Th36: :: TOPS_3:36
for X being non empty TopSpace
for A being Subset of X st A is open & A is dense holds
A is everywhere_dense
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X st A is open & A is dense holds
A is everywhere_dense
let A be Subset of X; ::_thesis: ( A is open & A is dense implies A is everywhere_dense )
assume  A is open ; ::_thesis: ( not A is dense or A is everywhere_dense )
then A1: A = Int A by TOPS_1:23;
assume  A is dense ; ::_thesis: A is everywhere_dense
hence  A is everywhere_dense by A1, Th35; ::_thesis: verum
end;

theorem :: TOPS_3:37
for X being non empty TopSpace
for A being Subset of X st A is everywhere_dense holds
not A is boundary
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X st A is everywhere_dense holds
not A is boundary
let A be Subset of X; ::_thesis: ( A is everywhere_dense implies not A is boundary )
assume  A is everywhere_dense ; ::_thesis: not A is boundary
then A1: Cl (Int A) = [#] X by Def4;
assume  A is boundary ; ::_thesis: contradiction
hence  contradiction by A1, PRE_TOPC:22; ::_thesis: verum
end;

theorem Th38: :: TOPS_3:38
for X being non empty TopSpace
for A, B being Subset of X st A is everywhere_dense & A c= B holds
B is everywhere_dense
proof
let X be non empty TopSpace; ::_thesis: for A, B being Subset of X st A is everywhere_dense & A c= B holds
B is everywhere_dense
let A, B be Subset of X; ::_thesis: ( A is everywhere_dense & A c= B implies B is everywhere_dense )
assume  A is everywhere_dense ; ::_thesis: ( not A c= B or B is everywhere_dense )
then A1: Cl (Int A) = [#] X by Def4;
assume  A c= B ; ::_thesis: B is everywhere_dense
then  Int A c= Int B by TOPS_1:19;
then  Cl (Int A) c= Cl (Int B) by PRE_TOPC:19;
then  [#] X = Cl (Int B) by A1, XBOOLE_0:def_10;
hence  B is everywhere_dense by Def4; ::_thesis: verum
end;

theorem Th39: :: TOPS_3:39
for X being non empty TopSpace
for A being Subset of X holds
( A is everywhere_dense iff A ` is nowhere_dense )
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X holds
( A is everywhere_dense iff A ` is nowhere_dense )
let A be Subset of X; ::_thesis: ( A is everywhere_dense iff A ` is nowhere_dense )
thus  ( A is everywhere_dense implies A ` is nowhere_dense ) ::_thesis: ( A ` is nowhere_dense implies A is everywhere_dense )
proof
assume  A is everywhere_dense ; ::_thesis: A ` is nowhere_dense
then  Cl (Int A) = [#] X by Def4;
then  (Cl (Int A)) ` = {} X by Th2;
then  Int ((Int A) `) = {} X by TDLAT_3:3;
then  Int (Cl (A `)) = {} by TDLAT_3:2;
then  Cl (A `) is boundary by TOPS_1:48;
hence  A ` is nowhere_dense by TOPS_1:def_5; ::_thesis: verum
end;
assume  A ` is nowhere_dense ; ::_thesis: A is everywhere_dense
then  Cl (A `) is boundary by TOPS_1:def_5;
then  Int (Cl (A `)) = {} X ;
then  Int ((Int A) `) = {} X by TDLAT_3:2;
then  (Cl (Int A)) ` = {} X by TDLAT_3:3;
then  Cl (Int A) = [#] X by Th2;
hence  A is everywhere_dense by Def4; ::_thesis: verum
end;

theorem Th40: :: TOPS_3:40
for X being non empty TopSpace
for A being Subset of X holds
( A is nowhere_dense iff A ` is everywhere_dense )
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X holds
( A is nowhere_dense iff A ` is everywhere_dense )
let A be Subset of X; ::_thesis: ( A is nowhere_dense iff A ` is everywhere_dense )
thus  ( A is nowhere_dense implies A ` is everywhere_dense ) ::_thesis: ( A ` is everywhere_dense implies A is nowhere_dense )
proof
assume  A is nowhere_dense ; ::_thesis: A ` is everywhere_dense
then  Cl A is boundary by TOPS_1:def_5;
then  Int (Cl A) = {} X ;
then  Int ((Int (A `)) `) = {} X by TDLAT_3:1;
then  (Cl (Int (A `))) ` = {} X by TDLAT_3:3;
then  Cl (Int (A `)) = [#] X by Th2;
hence  A ` is everywhere_dense by Def4; ::_thesis: verum
end;
assume  A ` is everywhere_dense ; ::_thesis: A is nowhere_dense
then  Cl (Int (A `)) = [#] X by Def4;
then  (Cl (Int (A `))) ` = {} X by Th2;
then  Int ((Int (A `)) `) = {} X by TDLAT_3:3;
then  Int (Cl A) = {} by TDLAT_3:1;
then  Cl A is boundary by TOPS_1:48;
hence  A is nowhere_dense by TOPS_1:def_5; ::_thesis: verum
end;

theorem Th41: :: TOPS_3:41
for X being non empty TopSpace
for A being Subset of X holds
( A is everywhere_dense iff ex C being Subset of X st
( C c= A & C is open & C is dense ) )
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X holds
( A is everywhere_dense iff ex C being Subset of X st
( C c= A & C is open & C is dense ) )
let A be Subset of X; ::_thesis: ( A is everywhere_dense iff ex C being Subset of X st
( C c= A & C is open & C is dense ) )
thus  ( A is everywhere_dense implies ex C being Subset of X st
( C c= A & C is open & C is dense ) ) ::_thesis: ( ex C being Subset of X st
( C c= A & C is open & C is dense ) implies A is everywhere_dense )
proof
assume A1: A is everywhere_dense ; ::_thesis: ex C being Subset of X st
( C c= A & C is open & C is dense )
take  Int A ; ::_thesis: ( Int A c= A & Int A is open & Int A is dense )
thus  ( Int A c= A & Int A is open & Int A is dense ) by A1, Th35, TOPS_1:16; ::_thesis: verum
end;
given C being Subset of X such that A2: ( C c= A & C is open & C is dense ) ; ::_thesis: A is everywhere_dense
 Int A is dense by A2, TOPS_1:24, TOPS_1:44;
hence  A is everywhere_dense by Th35; ::_thesis: verum
end;

theorem :: TOPS_3:42
for X being non empty TopSpace
for A being Subset of X holds
( A is everywhere_dense iff for F being Subset of X st F <> the carrier of X & F is closed holds
ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X ) )
proof
let X be non empty TopSpace; ::_thesis: for A being Subset of X holds
( A is everywhere_dense iff for F being Subset of X st F <> the carrier of X & F is closed holds
ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X ) )
let A be Subset of X; ::_thesis: ( A is everywhere_dense iff for F being Subset of X st F <> the carrier of X & F is closed holds
ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X ) )
thus  ( A is everywhere_dense implies for F being Subset of X st F <> the carrier of X & F is closed holds
ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X ) ) ::_thesis: ( ( for F being Subset of X st F <> the carrier of X & F is closed holds
ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X ) ) implies A is everywhere_dense )
proof
assume  A is everywhere_dense ; ::_thesis: for F being Subset of X st F <> the carrier of X & F is closed holds
ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X )
then A1: A ` is nowhere_dense by Th39;
let F be Subset of X; ::_thesis: ( F <> the carrier of X & F is closed implies ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X ) )
assume  F <> the carrier of X ; ::_thesis: ( not F is closed or ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X ) )
then A2: ([#] X) \ F <> {} by PRE_TOPC:4;
assume  F is closed ; ::_thesis: ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X )
then consider G being Subset of X such that
A3: G c= F ` and
A4: G <> {} and
A5: G is open and
A6: A ` misses G by A1, A2, Th28;
take H = G ` ; ::_thesis: ( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X )
 (F `) ` c= H by A3, SUBSET_1:12;
hence  F c= H ; ::_thesis: ( H <> the carrier of X & H is closed & A \/ H = the carrier of X )
 H ` <> {} by A4;
then  ([#] X) \ H <> {} ;
hence  H <> the carrier of X by PRE_TOPC:4; ::_thesis: ( H is closed & A \/ H = the carrier of X )
thus  H is closed by A5; ::_thesis: A \/ H = the carrier of X
 (A `) /\ (H `) = {} by A6, XBOOLE_0:def_7;
then  (A \/ H) ` = {} X by XBOOLE_1:53;
hence  A \/ H = the carrier of X by Th2; ::_thesis: verum
end;
assume A7: for F being Subset of X st F <> the carrier of X & F is closed holds
ex H being Subset of X st
( F c= H & H <> the carrier of X & H is closed & A \/ H = the carrier of X ) ; ::_thesis: A is everywhere_dense
 for G being Subset of X st G <> {} & G is open holds
ex H being Subset of X st
( H c= G & H <> {} & H is open & A ` misses H )
proof
let G be Subset of X; ::_thesis: ( G <> {} & G is open implies ex H being Subset of X st
( H c= G & H <> {} & H is open & A ` misses H ) )
assume  G <> {} ; ::_thesis: ( not G is open or ex H being Subset of X st
( H c= G & H <> {} & H is open & A ` misses H ) )
then  (G `) ` <> {} ;
then A8: G ` <> [#] X by PRE_TOPC:4;
assume  G is open ; ::_thesis: ex H being Subset of X st
( H c= G & H <> {} & H is open & A ` misses H )
then consider F being Subset of X such that
A9: G ` c= F and
A10: F <> the carrier of X and
A11: F is closed and
A12: A \/ F = the carrier of X by A7, A8;
take H = F ` ; ::_thesis: ( H c= G & H <> {} & H is open & A ` misses H )
 H c= (G `) ` by A9, SUBSET_1:12;
hence  H c= G ; ::_thesis: ( H <> {} & H is open & A ` misses H )
 F <> [#] X by A10;
hence  H <> {} by PRE_TOPC:4; ::_thesis: ( H is open & A ` misses H )
thus  H is open by A11; ::_thesis: A ` misses H
 (A \/ F) ` = {} X by A12, Th2;
hence  (A `) /\ H = {} by XBOOLE_1:53; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;
then  A ` is nowhere_dense by Th28;
hence  A is everywhere_dense by Th39; ::_thesis: verum
end;

theorem :: TOPS_3:43
for X being non empty TopSpace
for A, B being Subset of X st A is everywhere_dense holds
A \/ B is everywhere_dense by Th38, XBOOLE_1:7;

theorem Th44: :: TOPS_3:44
for X being non empty TopSpace
for A, B being Subset of X st A is everywhere_dense & B is everywhere_dense holds
A /\ B is everywhere_dense
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 /\ B is everywhere_dense
let A, B be Subset of X; ::_thesis: ( A is everywhere_dense & B is everywhere_dense implies A /\ B is everywhere_dense )
assume  ( A is everywhere_dense & B is everywhere_dense ) ; ::_thesis: A /\ B is everywhere_dense
then  ( A ` is nowhere_dense & B ` is nowhere_dense ) by Th39;
then  ( (A `) \/ (B `) = (A /\ B) ` & (A `) \/ (B `) is nowhere_dense ) by TOPS_1:53, XBOOLE_1:54;
hence  A /\ B is everywhere_dense by Th39; ::_thesis: verum
end;

theorem Th45: :: TOPS_3:45
for X being non empty TopSpace
for A, B being Subset of X st A is everywhere_dense & B is dense holds
A /\ B is dense
proof
let X be non empty TopSpace; ::_thesis: for A, B being Subset of X st A is everywhere_dense & B is dense holds
A /\ B is dense
let A, B be Subset of X; ::_thesis: ( A is everywhere_dense & B is dense implies A /\ B is dense )
assume  A is everywhere_dense ; ::_thesis: ( not B is dense or A /\ B is dense )
then A1: A ` is nowhere_dense by Th39;
assume  B is dense ; ::_thesis: A /\ B is dense
then  B ` is boundary by Th18;
then  ( (A `) \/ (B `) = (A /\ B) ` & (A `) \/ (B `) is boundary ) by A1, Th30, XBOOLE_1:54;
hence  A /\ B is dense by Th18; ::_thesis: verum
end;

theorem :: TOPS_3:46
for X being non empty TopSpace
for A, B being Subset of X st A is dense & B is nowhere_dense holds
A \ B is dense
proof
let X be non empty TopSpace; ::_thesis: for A, B being Subset of X st A is dense & B is nowhere_dense holds
A \ B is dense
let A, B be Subset of X; ::_thesis: ( A is dense & B is nowhere_dense implies A \ B is dense )
assume A1: A is dense ; ::_thesis: ( not B is nowhere_dense or A \ B is dense )
A2: A \ B = (B `) /\ A by SUBSET_1:13;
assume  B is nowhere_dense ; ::_thesis: A \ B is dense
then  B ` is everywhere_dense by Th40;
hence  A \ B is dense by A1, A2, Th45; ::_thesis: verum
end;

theorem :: TOPS_3:47
for X being non empty TopSpace
for A, B being Subset of X st A is everywhere_dense & B is boundary holds
A \ B is dense
proof
let X be non empty TopSpace; ::_thesis: for A, B being Subset of X st A is everywhere_dense & B is boundary holds
A \ B is dense
let A, B be Subset of X; ::_thesis: ( A is everywhere_dense & B is boundary implies A \ B is dense )
assume A1: A is everywhere_dense ; ::_thesis: ( not B is boundary or A \ B is dense )
A2: A \ B = A /\ (B `) by SUBSET_1:13;
assume  B is boundary ; ::_thesis: A \ B is dense
then  B ` is dense by TOPS_1:def_4;
hence  A \ B is dense by A1, A2, Th45; ::_thesis: verum
end;

theorem :: TOPS_3:48
for X being non empty TopSpace
for A, B being Subset of X st A is everywhere_dense & B is nowhere_dense holds
A \ B is everywhere_dense
proof
let X be non empty TopSpace; ::_thesis: for A, B being Subset of X st A is everywhere_dense & B is nowhere_dense holds
A \ B is everywhere_dense
let A, B be Subset of X; ::_thesis: ( A is everywhere_dense & B is nowhere_dense implies A \ B is everywhere_dense )
assume A1: A is everywhere_dense ; ::_thesis: ( not B is nowhere_dense or A \ B is everywhere_dense )
A2: A \ B = A /\ (B `) by SUBSET_1:13;
assume  B is nowhere_dense ; ::_thesis: A \ B is everywhere_dense
then  B ` is everywhere_dense by Th40;
hence  A \ B is everywhere_dense by A1, A2, Th44; ::_thesis: verum
end;

theorem :: TOPS_3:49
for X being non empty TopSpace
for D being Subset of X st D is everywhere_dense holds
ex C, B being Subset of X st
( C is open & C is dense & B is nowhere_dense & C \/ B = D & C misses B )
proof
let X be non empty TopSpace; ::_thesis: for D being Subset of X st D is everywhere_dense holds
ex C, B being Subset of X st
( C is open & C is dense & B is nowhere_dense & C \/ B = D & C misses B )
let D be Subset of X; ::_thesis: ( D is everywhere_dense implies ex C, B being Subset of X st
( C is open & C is dense & B is nowhere_dense & C \/ B = D & C misses B ) )
assume  D is everywhere_dense ; ::_thesis: ex C, B being Subset of X st
( C is open & C is dense & B is nowhere_dense & C \/ B = D & C misses B )
then consider C being Subset of X such that
A1: C c= D and
A2: ( C is open & C is dense ) by Th41;
take  C ; ::_thesis: ex B being Subset of X st
( C is open & C is dense & B is nowhere_dense & C \/ B = D & C misses B )
take B = D \ C; ::_thesis: ( C is open & C is dense & B is nowhere_dense & C \/ B = D & C misses B )
thus  ( C is open & C is dense ) by A2; ::_thesis: ( B is nowhere_dense & C \/ B = D & C misses B )
 C is everywhere_dense by A2, Th36;
then  C ` is nowhere_dense by Th39;
hence  B is nowhere_dense by Th26, XBOOLE_1:33; ::_thesis: ( C \/ B = D & C misses B )
thus  ( C \/ B = D & C misses B ) by A1, XBOOLE_1:45, XBOOLE_1:79; ::_thesis: verum
end;

theorem :: TOPS_3:50
for X being non empty TopSpace
for D being Subset of X st D is everywhere_dense holds
ex C, B being Subset of X st
( C is open & C is dense & B is closed & B is boundary & C \/ (D /\ B) = D & C misses B & C \/ B = the carrier of X )
proof
let X be non empty TopSpace; ::_thesis: for D being Subset of X st D is everywhere_dense holds
ex C, B being Subset of X st
( C is open & C is dense & B is closed & B is boundary & C \/ (D /\ B) = D & C misses B & C \/ B = the carrier of X )
let D be Subset of X; ::_thesis: ( D is everywhere_dense implies ex C, B being Subset of X st
( C is open & C is dense & B is closed & B is boundary & C \/ (D /\ B) = D & C misses B & C \/ B = the carrier of X ) )
assume  D is everywhere_dense ; ::_thesis: ex C, B being Subset of X st
( C is open & C is dense & B is closed & B is boundary & C \/ (D /\ B) = D & C misses B & C \/ B = the carrier of X )
then consider C being Subset of X such that
A1: C c= D and
A2: ( C is open & C is dense ) by Th41;
take  C ; ::_thesis: ex B being Subset of X st
( C is open & C is dense & B is closed & B is boundary & C \/ (D /\ B) = D & C misses B & C \/ B = the carrier of X )
take B = C ` ; ::_thesis: ( C is open & C is dense & B is closed & B is boundary & C \/ (D /\ B) = D & C misses B & C \/ B = the carrier of X )
thus  ( C is open & C is dense & B is closed & B is boundary ) by A2, Th18; ::_thesis: ( C \/ (D /\ B) = D & C misses B & C \/ B = the carrier of X )
thus C \/ (D /\ B) = (C \/ D) /\ (C \/ (C `)) by XBOOLE_1:24
.= (C \/ D) /\ ([#] X) by PRE_TOPC:2
.= C \/ D by XBOOLE_1:28
.= D by A1, XBOOLE_1:12 ; ::_thesis: ( C misses B & C \/ B = the carrier of X )
 C misses B by XBOOLE_1:79;
hence  C /\ B = {} by XBOOLE_0:def_7; :: according to XBOOLE_0:def_7 ::_thesis: C \/ B = the carrier of X
 C \/ B = [#] X by PRE_TOPC:2;
hence  C \/ B = the carrier of X ; ::_thesis: verum
end;

theorem :: TOPS_3:51
for X being non empty TopSpace
for D being Subset of X st D is nowhere_dense holds
ex C, B being Subset of X st
( C is closed & C is boundary & B is everywhere_dense & C /\ B = D & C \/ B = the carrier of X )
proof
let X be non empty TopSpace; ::_thesis: for D being Subset of X st D is nowhere_dense holds
ex C, B being Subset of X st
( C is closed & C is boundary & B is everywhere_dense & C /\ B = D & C \/ B = the carrier of X )
let D be Subset of X; ::_thesis: ( D is nowhere_dense implies ex C, B being Subset of X st
( C is closed & C is boundary & B is everywhere_dense & C /\ B = D & C \/ B = the carrier of X ) )
assume  D is nowhere_dense ; ::_thesis: ex C, B being Subset of X st
( C is closed & C is boundary & B is everywhere_dense & C /\ B = D & C \/ B = the carrier of X )
then consider C being Subset of X such that
A1: D c= C and
A2: ( C is closed & C is boundary ) by Th27;
take  C ; ::_thesis: ex B being Subset of X st
( C is closed & C is boundary & B is everywhere_dense & C /\ B = D & C \/ B = the carrier of X )
take B = D \/ (C `); ::_thesis: ( C is closed & C is boundary & B is everywhere_dense & C /\ B = D & C \/ B = the carrier of X )
thus  ( C is closed & C is boundary ) by A2; ::_thesis: ( B is everywhere_dense & C /\ B = D & C \/ B = the carrier of X )
 C ` is everywhere_dense by A2, Th40;
hence  B is everywhere_dense by Th38, XBOOLE_1:7; ::_thesis: ( C /\ B = D & C \/ B = the carrier of X )
A3: C misses C ` by XBOOLE_1:79;
thus C /\ B = (C /\ D) \/ (C /\ (C `)) by XBOOLE_1:23
.= (C /\ D) \/ ({} X) by A3, XBOOLE_0:def_7
.= D by A1, XBOOLE_1:28 ; ::_thesis: C \/ B = the carrier of X
thus C \/ B = D \/ (C \/ (C `)) by XBOOLE_1:4
.= D \/ ([#] X) by PRE_TOPC:2
.= the carrier of X by XBOOLE_1:12 ; ::_thesis: verum
end;

theorem :: TOPS_3:52
for X being non empty TopSpace
for D being Subset of X st D is nowhere_dense holds
ex C, B being Subset of X st
( C is closed & C is boundary & B is open & B is dense & C /\ (D \/ B) = D & C misses B & C \/ B = the carrier of X )
proof
let X be non empty TopSpace; ::_thesis: for D being Subset of X st D is nowhere_dense holds
ex C, B being Subset of X st
( C is closed & C is boundary & B is open & B is dense & C /\ (D \/ B) = D & C misses B & C \/ B = the carrier of X )
let D be Subset of X; ::_thesis: ( D is nowhere_dense implies ex C, B being Subset of X st
( C is closed & C is boundary & B is open & B is dense & C /\ (D \/ B) = D & C misses B & C \/ B = the carrier of X ) )
assume  D is nowhere_dense ; ::_thesis: ex C, B being Subset of X st
( C is closed & C is boundary & B is open & B is dense & C /\ (D \/ B) = D & C misses B & C \/ B = the carrier of X )
then consider C being Subset of X such that
A1: D c= C and
A2: ( C is closed & C is boundary ) by Th27;
take  C ; ::_thesis: ex B being Subset of X st
( C is closed & C is boundary & B is open & B is dense & C /\ (D \/ B) = D & C misses B & C \/ B = the carrier of X )
take B = C ` ; ::_thesis: ( C is closed & C is boundary & B is open & B is dense & C /\ (D \/ B) = D & C misses B & C \/ B = the carrier of X )
thus  ( C is closed & C is boundary & B is open & B is dense ) by A2; ::_thesis: ( C /\ (D \/ B) = D & C misses B & C \/ B = the carrier of X )
A3: C misses C ` by XBOOLE_1:79;
thus C /\ (D \/ B) = (C /\ D) \/ (C /\ (C `)) by XBOOLE_1:23
.= (C /\ D) \/ ({} X) by A3, XBOOLE_0:def_7
.= D by A1, XBOOLE_1:28 ; ::_thesis: ( C misses B & C \/ B = the carrier of X )
 C misses B by XBOOLE_1:79;
hence  C /\ B = {} by XBOOLE_0:def_7; :: according to XBOOLE_0:def_7 ::_thesis: C \/ B = the carrier of X
 C \/ B = [#] X by PRE_TOPC:2;
hence  C \/ B = the carrier of X ; ::_thesis: verum
end;

begin

theorem Th53: :: TOPS_3:53
for X being non empty TopSpace
for Y0 being SubSpace of X
for A being Subset of X
for B being Subset of Y0 st B c= A holds
Cl B c= Cl A
proof
let X be non empty TopSpace; ::_thesis: for Y0 being SubSpace of X
for A being Subset of X
for B being Subset of Y0 st B c= A holds
Cl B c= Cl A
let Y0 be SubSpace of X; ::_thesis: for A being Subset of X
for B being Subset of Y0 st B c= A holds
Cl B c= Cl A
let A be Subset of X; ::_thesis: for B being Subset of Y0 st B c= A holds
Cl B c= Cl A
let B be Subset of Y0; ::_thesis: ( B c= A implies Cl B c= Cl A )
assume A1: B c= A ; ::_thesis: Cl B c= Cl A
then reconsider D = B as Subset of X by XBOOLE_1:1;
 Cl B = (Cl D) /\ ([#] Y0) by PRE_TOPC:17;
then A2: Cl B c= Cl D by XBOOLE_1:17;
 Cl D c= Cl A by A1, PRE_TOPC:19;
hence  Cl B c= Cl A by A2, XBOOLE_1:1; ::_thesis: verum
end;

theorem Th54: :: TOPS_3:54
for X being non empty TopSpace
for Y0 being SubSpace of X
for C, A being Subset of X
for B being Subset of Y0 st C is closed & C c= the carrier of Y0 & A c= C & A = B holds
Cl A = Cl B
proof
let X be non empty TopSpace; ::_thesis: for Y0 being SubSpace of X
for C, A being Subset of X
for B being Subset of Y0 st C is closed & C c= the carrier of Y0 & A c= C & A = B holds
Cl A = Cl B
let Y0 be SubSpace of X; ::_thesis: for C, A being Subset of X
for B being Subset of Y0 st C is closed & C c= the carrier of Y0 & A c= C & A = B holds
Cl A = Cl B
let C, A be Subset of X; ::_thesis: for B being Subset of Y0 st C is closed & C c= the carrier of Y0 & A c= C & A = B holds
Cl A = Cl B
let B be Subset of Y0; ::_thesis: ( C is closed & C c= the carrier of Y0 & A c= C & A = B implies Cl A = Cl B )
assume A1: C is closed ; ::_thesis: ( not C c= the carrier of Y0 or not A c= C or not A = B or Cl A = Cl B )
assume A2: C c= the carrier of Y0 ; ::_thesis: ( not A c= C or not A = B or Cl A = Cl B )
assume  A c= C ; ::_thesis: ( not A = B or Cl A = Cl B )
then  Cl A c= Cl C by PRE_TOPC:19;
then  Cl A c= C by A1, PRE_TOPC:22;
then A3: Cl A = (Cl A) /\ ([#] Y0) by A2, XBOOLE_1:1, XBOOLE_1:28;
assume  A = B ; ::_thesis: Cl A = Cl B
hence  Cl A = Cl B by A3, PRE_TOPC:17; ::_thesis: verum
end;

theorem :: TOPS_3:55
for X being non empty TopSpace
for Y0 being non empty closed SubSpace of X
for A being Subset of X
for B being Subset of Y0 st A = B holds
Cl A = Cl B
proof
let X be non empty TopSpace; ::_thesis: for Y0 being non empty closed SubSpace of X
for A being Subset of X
for B being Subset of Y0 st A = B holds
Cl A = Cl B
let Y0 be non empty closed SubSpace of X; ::_thesis: for A being Subset of X
for B being Subset of Y0 st A = B holds
Cl A = Cl B
reconsider C = the carrier of Y0 as Subset of X by TSEP_1:1;
let A be Subset of X; ::_thesis: for B being Subset of Y0 st A = B holds
Cl A = Cl B
let B be Subset of Y0; ::_thesis: ( A = B implies Cl A = Cl B )
A1: C is closed by TSEP_1:11;
assume  A = B ; ::_thesis: Cl A = Cl B
hence  Cl A = Cl B by A1, Th54; ::_thesis: verum
end;

theorem Th56: :: TOPS_3:56
for X being non empty TopSpace
for Y0 being SubSpace of X
for A being Subset of X
for B being Subset of Y0 st A c= B holds
Int A c= Int B
proof
let X be non empty TopSpace; ::_thesis: for Y0 being SubSpace of X
for A being Subset of X
for B being Subset of Y0 st A c= B holds
Int A c= Int B
let Y0 be SubSpace of X; ::_thesis: for A being Subset of X
for B being Subset of Y0 st A c= B holds
Int A c= Int B
let A be Subset of X; ::_thesis: for B being Subset of Y0 st A c= B holds
Int A c= Int B
let B be Subset of Y0; ::_thesis: ( A c= B implies Int A c= Int B )
A1: Int A c= A by TOPS_1:16;
assume  A c= B ; ::_thesis: Int A c= Int B
then A2: Int A c= B by A1, XBOOLE_1:1;
then reconsider C = Int A as Subset of Y0 by XBOOLE_1:1;
 C is open by TOPS_2:25;
hence  Int A c= Int B by A2, TOPS_1:24; ::_thesis: verum
end;

theorem Th57: :: TOPS_3:57
for X being non empty TopSpace
for Y0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of Y0 st C is open & C c= the carrier of Y0 & A c= C & A = B holds
Int A = Int B
proof
let X be non empty TopSpace; ::_thesis: for Y0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of Y0 st C is open & C c= the carrier of Y0 & A c= C & A = B holds
Int A = Int B
let Y0 be non empty SubSpace of X; ::_thesis: for C, A being Subset of X
for B being Subset of Y0 st C is open & C c= the carrier of Y0 & A c= C & A = B holds
Int A = Int B
let C, A be Subset of X; ::_thesis: for B being Subset of Y0 st C is open & C c= the carrier of Y0 & A c= C & A = B holds
Int A = Int B
let B be Subset of Y0; ::_thesis: ( C is open & C c= the carrier of Y0 & A c= C & A = B implies Int A = Int B )
assume A1: C is open ; ::_thesis: ( not C c= the carrier of Y0 or not A c= C or not A = B or Int A = Int B )
assume A2: C c= the carrier of Y0 ; ::_thesis: ( not A c= C or not A = B or Int A = Int B )
assume A3: A c= C ; ::_thesis: ( not A = B or Int A = Int B )
assume A4: A = B ; ::_thesis: Int A = Int B
A5: Int B c= B by TOPS_1:16;
then reconsider D = Int B as Subset of X by A4, XBOOLE_1:1;
 Int B c= C by A3, A4, A5, XBOOLE_1:1;
then  D is open by A1, A2, TSEP_1:9;
then A6: D c= Int A by A4, TOPS_1:16, TOPS_1:24;
 Int A c= Int B by A4, Th56;
hence  Int A = Int B by A6, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: TOPS_3:58
for X being non empty TopSpace
for Y0 being non empty open SubSpace of X
for A being Subset of X
for B being Subset of Y0 st A = B holds
Int A = Int B
proof
let X be non empty TopSpace; ::_thesis: for Y0 being non empty open SubSpace of X
for A being Subset of X
for B being Subset of Y0 st A = B holds
Int A = Int B
let Y0 be non empty open SubSpace of X; ::_thesis: for A being Subset of X
for B being Subset of Y0 st A = B holds
Int A = Int B
reconsider C = the carrier of Y0 as Subset of X by TSEP_1:1;
let A be Subset of X; ::_thesis: for B being Subset of Y0 st A = B holds
Int A = Int B
let B be Subset of Y0; ::_thesis: ( A = B implies Int A = Int B )
A1: C is open by TSEP_1:16;
assume  A = B ; ::_thesis: Int A = Int B
hence  Int A = Int B by A1, Th57; ::_thesis: verum
end;

theorem Th59: :: TOPS_3:59
for X being non empty TopSpace
for X0 being SubSpace of X
for A being Subset of X
for B being Subset of X0 st A c= B & A is dense holds
B is dense
proof
let X be non empty TopSpace; ::_thesis: for X0 being SubSpace of X
for A being Subset of X
for B being Subset of X0 st A c= B & A is dense holds
B is dense
let X0 be SubSpace of X; ::_thesis: for A being Subset of X
for B being Subset of X0 st A c= B & A is dense holds
B is dense
let A be Subset of X; ::_thesis: for B being Subset of X0 st A c= B & A is dense holds
B is dense
let B be Subset of X0; ::_thesis: ( A c= B & A is dense implies B is dense )
A1: [#] X0 c= [#] X by PRE_TOPC:def_4;
assume A2: A c= B ; ::_thesis: ( not A is dense or B is dense )
then reconsider C = A as Subset of X0 by XBOOLE_1:1;
assume  A is dense ; ::_thesis: B is dense
then  Cl A = [#] X by TOPS_1:def_3;
then  [#] X0 = (Cl A) /\ ([#] X0) by A1, XBOOLE_1:28;
then  Cl C = [#] X0 by PRE_TOPC:17;
then  C is dense by TOPS_1:def_3;
hence  B is dense by A2, TOPS_1:44; ::_thesis: verum
end;

theorem Th60: :: TOPS_3:60
for X being non empty TopSpace
for X0 being SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C c= the carrier of X0 & A c= C & A = B holds
( ( C is dense & B is dense ) iff A is dense )
proof
let X be non empty TopSpace; ::_thesis: for X0 being SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C c= the carrier of X0 & A c= C & A = B holds
( ( C is dense & B is dense ) iff A is dense )
let X0 be SubSpace of X; ::_thesis: for C, A being Subset of X
for B being Subset of X0 st C c= the carrier of X0 & A c= C & A = B holds
( ( C is dense & B is dense ) iff A is dense )
let C, A be Subset of X; ::_thesis: for B being Subset of X0 st C c= the carrier of X0 & A c= C & A = B holds
( ( C is dense & B is dense ) iff A is dense )
let B be Subset of X0; ::_thesis: ( C c= the carrier of X0 & A c= C & A = B implies ( ( C is dense & B is dense ) iff A is dense ) )
assume A1: C c= the carrier of X0 ; ::_thesis: ( not A c= C or not A = B or ( ( C is dense & B is dense ) iff A is dense ) )
reconsider P = the carrier of X0 as Subset of X by TSEP_1:1;
assume A2: A c= C ; ::_thesis: ( not A = B or ( ( C is dense & B is dense ) iff A is dense ) )
assume A3: A = B ; ::_thesis: ( ( C is dense & B is dense ) iff A is dense )
thus  ( C is dense & B is dense implies A is dense ) ::_thesis: ( A is dense implies ( C is dense & B is dense ) )
proof
assume  C is dense ; ::_thesis: ( not B is dense or A is dense )
then  Cl C = [#] X by TOPS_1:def_3;
then A4: [#] X c= Cl P by A1, PRE_TOPC:19;
assume  B is dense ; ::_thesis: A is dense
then  Cl B = [#] X0 by TOPS_1:def_3;
then  P = (Cl A) /\ ([#] X0) by A3, PRE_TOPC:17;
then  Cl P c= Cl (Cl A) by PRE_TOPC:19, XBOOLE_1:17;
then  [#] X c= Cl A by A4, XBOOLE_1:1;
then  Cl A = [#] X by XBOOLE_0:def_10;
hence  A is dense by TOPS_1:def_3; ::_thesis: verum
end;
thus  ( A is dense implies ( C is dense & B is dense ) ) by A2, A3, Th59, TOPS_1:44; ::_thesis: verum
end;

theorem Th61: :: TOPS_3:61
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for A being Subset of X
for B being Subset of X0 st A c= B & A is everywhere_dense holds
B is everywhere_dense
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty SubSpace of X
for A being Subset of X
for B being Subset of X0 st A c= B & A is everywhere_dense holds
B is everywhere_dense
let X0 be non empty SubSpace of X; ::_thesis: for A being Subset of X
for B being Subset of X0 st A c= B & A is everywhere_dense holds
B is everywhere_dense
let A be Subset of X; ::_thesis: for B being Subset of X0 st A c= B & A is everywhere_dense holds
B is everywhere_dense
let B be Subset of X0; ::_thesis: ( A c= B & A is everywhere_dense implies B is everywhere_dense )
assume A1: A c= B ; ::_thesis: ( not A is everywhere_dense or B is everywhere_dense )
then reconsider C = A as Subset of X0 by XBOOLE_1:1;
assume  A is everywhere_dense ; ::_thesis: B is everywhere_dense
then  Int A is dense by Th35;
then  Int C is dense by Th56, Th59;
then  Int B is dense by A1, TOPS_1:19, TOPS_1:44;
hence  B is everywhere_dense by Th35; ::_thesis: verum
end;

theorem Th62: :: TOPS_3:62
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B holds
( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B holds
( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )
let X0 be non empty SubSpace of X; ::_thesis: for C, A being Subset of X
for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B holds
( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )
let C, A be Subset of X; ::_thesis: for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B holds
( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )
let B be Subset of X0; ::_thesis: ( C is open & C c= the carrier of X0 & A c= C & A = B implies ( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense ) )
assume A1: C is open ; ::_thesis: ( not C c= the carrier of X0 or not A c= C or not A = B or ( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense ) )
assume  C c= the carrier of X0 ; ::_thesis: ( not A c= C or not A = B or ( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense ) )
then reconsider E = C as Subset of X0 ;
A2: E is open by A1, TOPS_2:25;
assume A3: A c= C ; ::_thesis: ( not A = B or ( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense ) )
assume A4: A = B ; ::_thesis: ( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )
A5: Int B c= B by TOPS_1:16;
then reconsider D = Int B as Subset of X by A4, XBOOLE_1:1;
 Int B c= Int E by A3, A4, TOPS_1:19;
then A6: Int B c= E by A2, TOPS_1:23;
then A7: D is open by A1, TSEP_1:9;
thus  ( C is dense & B is everywhere_dense implies A is everywhere_dense ) ::_thesis: ( A is everywhere_dense implies ( C is dense & B is everywhere_dense ) )
proof
assume A8: C is dense ; ::_thesis: ( not B is everywhere_dense or A is everywhere_dense )
assume  B is everywhere_dense ; ::_thesis: A is everywhere_dense
then  Int B is dense by Th35;
then  D is dense by A6, A8, Th60;
then  Int A is dense by A4, A5, A7, TOPS_1:24, TOPS_1:44;
hence  A is everywhere_dense by Th35; ::_thesis: verum
end;
thus  ( A is everywhere_dense implies ( C is dense & B is everywhere_dense ) ) ::_thesis: verum
proof
assume A9: A is everywhere_dense ; ::_thesis: ( C is dense & B is everywhere_dense )
hence  C is dense by A3, Th33, Th38; ::_thesis: B is everywhere_dense
thus  B is everywhere_dense by A4, A9, Th61; ::_thesis: verum
end;
end;

theorem :: TOPS_3:63
for X being non empty TopSpace
for X0 being non empty open SubSpace of X
for A, C being Subset of X
for B being Subset of X0 st C = the carrier of X0 & A = B holds
( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty open SubSpace of X
for A, C being Subset of X
for B being Subset of X0 st C = the carrier of X0 & A = B holds
( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )
let X0 be non empty open SubSpace of X; ::_thesis: for A, C being Subset of X
for B being Subset of X0 st C = the carrier of X0 & A = B holds
( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )
let A, C be Subset of X; ::_thesis: for B being Subset of X0 st C = the carrier of X0 & A = B holds
( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )
let B be Subset of X0; ::_thesis: ( C = the carrier of X0 & A = B implies ( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense ) )
assume A1: C = the carrier of X0 ; ::_thesis: ( not A = B or ( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense ) )
assume A2: A = B ; ::_thesis: ( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense )
 C is open by A1, TSEP_1:def_1;
hence  ( ( C is dense & B is everywhere_dense ) iff A is everywhere_dense ) by A1, A2, Th62; ::_thesis: verum
end;

theorem :: TOPS_3:64
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C c= the carrier of X0 & A c= C & A = B holds
( ( C is everywhere_dense & B is everywhere_dense ) iff A is everywhere_dense )
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C c= the carrier of X0 & A c= C & A = B holds
( ( C is everywhere_dense & B is everywhere_dense ) iff A is everywhere_dense )
let X0 be non empty SubSpace of X; ::_thesis: for C, A being Subset of X
for B being Subset of X0 st C c= the carrier of X0 & A c= C & A = B holds
( ( C is everywhere_dense & B is everywhere_dense ) iff A is everywhere_dense )
let C, A be Subset of X; ::_thesis: for B being Subset of X0 st C c= the carrier of X0 & A c= C & A = B holds
( ( C is everywhere_dense & B is everywhere_dense ) iff A is everywhere_dense )
let B be Subset of X0; ::_thesis: ( C c= the carrier of X0 & A c= C & A = B implies ( ( C is everywhere_dense & B is everywhere_dense ) iff A is everywhere_dense ) )
assume A1: C c= the carrier of X0 ; ::_thesis: ( not A c= C or not A = B or ( ( C is everywhere_dense & B is everywhere_dense ) iff A is everywhere_dense ) )
assume A2: A c= C ; ::_thesis: ( not A = B or ( ( C is everywhere_dense & B is everywhere_dense ) iff A is everywhere_dense ) )
assume A3: A = B ; ::_thesis: ( ( C is everywhere_dense & B is everywhere_dense ) iff A is everywhere_dense )
thus  ( C is everywhere_dense & B is everywhere_dense implies A is everywhere_dense ) ::_thesis: ( A is everywhere_dense implies ( C is everywhere_dense & B is everywhere_dense ) )
proof
 Int C c= C by TOPS_1:16;
then reconsider D = Int C as Subset of X0 by A1, XBOOLE_1:1;
A4: D /\ B c= Int C by XBOOLE_1:17;
then reconsider E = D /\ B as Subset of X by XBOOLE_1:1;
assume A5: C is everywhere_dense ; ::_thesis: ( not B is everywhere_dense or A is everywhere_dense )
then  Int C is everywhere_dense by Th32;
then A6: D is everywhere_dense by Th61;
assume  B is everywhere_dense ; ::_thesis: A is everywhere_dense
then A7: D /\ B is everywhere_dense by A6, Th44;
 Int C is dense by A5, Th32, Th33;
then  E is everywhere_dense by A7, A4, Th62;
hence  A is everywhere_dense by A3, Th38, XBOOLE_1:17; ::_thesis: verum
end;
thus  ( A is everywhere_dense implies ( C is everywhere_dense & B is everywhere_dense ) ) by A2, A3, Th38, Th61; ::_thesis: verum
end;

theorem Th65: :: TOPS_3:65
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for A being Subset of X
for B being Subset of X0 st A c= B & B is boundary holds
A is boundary
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty SubSpace of X
for A being Subset of X
for B being Subset of X0 st A c= B & B is boundary holds
A is boundary
let X0 be non empty SubSpace of X; ::_thesis: for A being Subset of X
for B being Subset of X0 st A c= B & B is boundary holds
A is boundary
let A be Subset of X; ::_thesis: for B being Subset of X0 st A c= B & B is boundary holds
A is boundary
let B be Subset of X0; ::_thesis: ( A c= B & B is boundary implies A is boundary )
assume A1: A c= B ; ::_thesis: ( not B is boundary or A is boundary )
then reconsider C = A as Subset of X0 by XBOOLE_1:1;
assume  Int B = {} ; :: according to TOPS_3:def_1 ::_thesis: A is boundary
then  Int C = {} by A1, TOPS_1:19, XBOOLE_1:3;
then  Int A = {} by Th56, XBOOLE_1:3;
hence  A is boundary by Def1; ::_thesis: verum
end;

theorem Th66: :: TOPS_3:66
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B & A is boundary holds
B is boundary
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B & A is boundary holds
B is boundary
let X0 be non empty SubSpace of X; ::_thesis: for C, A being Subset of X
for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B & A is boundary holds
B is boundary
let C, A be Subset of X; ::_thesis: for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B & A is boundary holds
B is boundary
let B be Subset of X0; ::_thesis: ( C is open & C c= the carrier of X0 & A c= C & A = B & A is boundary implies B is boundary )
assume  ( C is open & C c= the carrier of X0 & A c= C & A = B ) ; ::_thesis: ( not A is boundary or B is boundary )
then A1: Int A = Int B by Th57;
assume  A is boundary ; ::_thesis: B is boundary
then  Int A = {} ;
hence  B is boundary by A1, TOPS_1:48; ::_thesis: verum
end;

theorem :: TOPS_3:67
for X being non empty TopSpace
for X0 being non empty open SubSpace of X
for A being Subset of X
for B being Subset of X0 st A = B holds
( A is boundary iff B is boundary )
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty open SubSpace of X
for A being Subset of X
for B being Subset of X0 st A = B holds
( A is boundary iff B is boundary )
let X0 be non empty open SubSpace of X; ::_thesis: for A being Subset of X
for B being Subset of X0 st A = B holds
( A is boundary iff B is boundary )
let A be Subset of X; ::_thesis: for B being Subset of X0 st A = B holds
( A is boundary iff B is boundary )
let B be Subset of X0; ::_thesis: ( A = B implies ( A is boundary iff B is boundary ) )
reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
A1: C is open by TSEP_1:def_1;
assume  A = B ; ::_thesis: ( A is boundary iff B is boundary )
hence  ( A is boundary iff B is boundary ) by A1, Th65, Th66; ::_thesis: verum
end;

theorem Th68: :: TOPS_3:68
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for A being Subset of X
for B being Subset of X0 st A c= B & B is nowhere_dense holds
A is nowhere_dense
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty SubSpace of X
for A being Subset of X
for B being Subset of X0 st A c= B & B is nowhere_dense holds
A is nowhere_dense
let X0 be non empty SubSpace of X; ::_thesis: for A being Subset of X
for B being Subset of X0 st A c= B & B is nowhere_dense holds
A is nowhere_dense
let A be Subset of X; ::_thesis: for B being Subset of X0 st A c= B & B is nowhere_dense holds
A is nowhere_dense
let B be Subset of X0; ::_thesis: ( A c= B & B is nowhere_dense implies A is nowhere_dense )
reconsider D = the carrier of X0 as Subset of X by TSEP_1:1;
reconsider G = (Int (Cl A)) /\ ([#] X0) as Subset of X0 ;
assume A1: A c= B ; ::_thesis: ( not B is nowhere_dense or A is nowhere_dense )
then reconsider C = A as Subset of X0 by XBOOLE_1:1;
assume  B is nowhere_dense ; ::_thesis: A is nowhere_dense
then  C is nowhere_dense by A1, Th26;
then A2: ( G is open & Int (Cl C) = {} ) by Def3, TOPS_2:24;
 (Int (Cl A)) /\ ([#] X0) c= (Cl A) /\ ([#] X0) by TOPS_1:16, XBOOLE_1:26;
then A3: (Int (Cl A)) /\ ([#] X0) c= Cl C by PRE_TOPC:17;
now__::_thesis:_not_Int_(Cl_A)_<>_{}
assume  Int (Cl A) <> {} ; ::_thesis: contradiction
then  A meets Int (Cl A) by Th7;
then A4: A /\ (Int (Cl A)) <> {} by XBOOLE_0:def_7;
 C c= D ;
then  (Int (Cl A)) /\ D <> {} by A4, XBOOLE_1:3, XBOOLE_1:26;
hence  contradiction by A3, A2, TOPS_1:24, XBOOLE_1:3; ::_thesis: verum
end;
hence  A is nowhere_dense by Def3; ::_thesis: verum
end;

Lm1:  for X being non empty TopSpace
for X0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C is open & C = the carrier of X0 & A = B & A is nowhere_dense holds
B is nowhere_dense
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C is open & C = the carrier of X0 & A = B & A is nowhere_dense holds
B is nowhere_dense
let X0 be non empty SubSpace of X; ::_thesis: for C, A being Subset of X
for B being Subset of X0 st C is open & C = the carrier of X0 & A = B & A is nowhere_dense holds
B is nowhere_dense
let C, A be Subset of X; ::_thesis: for B being Subset of X0 st C is open & C = the carrier of X0 & A = B & A is nowhere_dense holds
B is nowhere_dense
let B be Subset of X0; ::_thesis: ( C is open & C = the carrier of X0 & A = B & A is nowhere_dense implies B is nowhere_dense )
assume A1: C is open ; ::_thesis: ( not C = the carrier of X0 or not A = B or not A is nowhere_dense or B is nowhere_dense )
assume A2: C = the carrier of X0 ; ::_thesis: ( not A = B or not A is nowhere_dense or B is nowhere_dense )
assume  A = B ; ::_thesis: ( not A is nowhere_dense or B is nowhere_dense )
then A3: Cl B c= Cl A by Th53;
then reconsider D = Cl B as Subset of X by XBOOLE_1:1;
assume  A is nowhere_dense ; ::_thesis: B is nowhere_dense
then A4: Int (Cl A) = {} by Def3;
 Int D = Int (Cl B) by A1, A2, Th57;
then  Int (Cl B) = {} by A3, A4, TOPS_1:19, XBOOLE_1:3;
hence  B is nowhere_dense by Def3; ::_thesis: verum
end;

theorem Th69: :: TOPS_3:69
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B & A is nowhere_dense holds
B is nowhere_dense
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B & A is nowhere_dense holds
B is nowhere_dense
let X0 be non empty SubSpace of X; ::_thesis: for C, A being Subset of X
for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B & A is nowhere_dense holds
B is nowhere_dense
let C, A be Subset of X; ::_thesis: for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B & A is nowhere_dense holds
B is nowhere_dense
let B be Subset of X0; ::_thesis: ( C is open & C c= the carrier of X0 & A c= C & A = B & A is nowhere_dense implies B is nowhere_dense )
assume A1: C is open ; ::_thesis: ( not C c= the carrier of X0 or not A c= C or not A = B or not A is nowhere_dense or B is nowhere_dense )
assume A2: C c= the carrier of X0 ; ::_thesis: ( not A c= C or not A = B or not A is nowhere_dense or B is nowhere_dense )
assume that
A3: A c= C and
A4: A = B ; ::_thesis: ( not A is nowhere_dense or B is nowhere_dense )
assume A5: A is nowhere_dense ; ::_thesis: B is nowhere_dense
A6: now__::_thesis:_(_C_<>_{}_implies_B_is_nowhere_dense_)
assume  C <> {} ; ::_thesis: B is nowhere_dense
then consider X1 being non empty strict SubSpace of X such that
A7: C = the carrier of X1 by TSEP_1:10;
reconsider E = B as Subset of X1 by A3, A4, A7;
 ( E is nowhere_dense & X1 is SubSpace of X0 ) by A1, A2, A4, A5, A7, Lm1, TSEP_1:4;
hence  B is nowhere_dense by Th68; ::_thesis: verum
end;
now__::_thesis:_(_C_=_{}_implies_B_is_nowhere_dense_)
assume  C = {} ; ::_thesis: B is nowhere_dense
then  B = {} X0 by A3, A4, XBOOLE_1:3;
hence  B is nowhere_dense ; ::_thesis: verum
end;
hence  B is nowhere_dense by A6; ::_thesis: verum
end;

theorem :: TOPS_3:70
for X being non empty TopSpace
for X0 being non empty open SubSpace of X
for A being Subset of X
for B being Subset of X0 st A = B holds
( A is nowhere_dense iff B is nowhere_dense )
proof
let X be non empty TopSpace; ::_thesis: for X0 being non empty open SubSpace of X
for A being Subset of X
for B being Subset of X0 st A = B holds
( A is nowhere_dense iff B is nowhere_dense )
let X0 be non empty open SubSpace of X; ::_thesis: for A being Subset of X
for B being Subset of X0 st A = B holds
( A is nowhere_dense iff B is nowhere_dense )
let A be Subset of X; ::_thesis: for B being Subset of X0 st A = B holds
( A is nowhere_dense iff B is nowhere_dense )
let B be Subset of X0; ::_thesis: ( A = B implies ( A is nowhere_dense iff B is nowhere_dense ) )
reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
A1: C is open by TSEP_1:def_1;
assume  A = B ; ::_thesis: ( A is nowhere_dense iff B is nowhere_dense )
hence  ( A is nowhere_dense iff B is nowhere_dense ) by A1, Th68, Th69; ::_thesis: verum
end;

begin

theorem :: TOPS_3:71
for X1, X2 being 1-sorted st the carrier of X1 = the carrier of X2 holds
for C1 being Subset of X1
for C2 being Subset of X2 holds
( C1 = C2 iff C1 ` = C2 ` )
proof
let X1, X2 be 1-sorted ; ::_thesis: ( the carrier of X1 = the carrier of X2 implies for C1 being Subset of X1
for C2 being Subset of X2 holds
( C1 = C2 iff C1 ` = C2 ` ) )
assume A1: the carrier of X1 = the carrier of X2 ; ::_thesis: for C1 being Subset of X1
for C2 being Subset of X2 holds
( C1 = C2 iff C1 ` = C2 ` )
let C1 be Subset of X1; ::_thesis: for C2 being Subset of X2 holds
( C1 = C2 iff C1 ` = C2 ` )
let C2 be Subset of X2; ::_thesis: ( C1 = C2 iff C1 ` = C2 ` )
thus  ( C1 = C2 implies C1 ` = C2 ` ) by A1; ::_thesis: ( C1 ` = C2 ` implies C1 = C2 )
thus  ( C1 ` = C2 ` implies C1 = C2 ) ::_thesis: verum
proof
assume  C1 ` = C2 ` ; ::_thesis: C1 = C2
hence C1 = ([#] X2) \ (C2 `) by A1, PRE_TOPC:3
.= C2 by PRE_TOPC:3 ;
::_thesis: verum
end;
end;


theorem Th72: :: TOPS_3:72
for X1, X2 being TopStruct st the carrier of X1 = the carrier of X2 & ( for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
( C1 is open iff C2 is open ) ) holds
TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
proof
let X1, X2 be TopStruct ; ::_thesis: ( the carrier of X1 = the carrier of X2 & ( for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
( C1 is open iff C2 is open ) ) implies TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) )
assume A1: the carrier of X1 = the carrier of X2 ; ::_thesis: ( ex C1 being Subset of X1 ex C2 being Subset of X2 st
( C1 = C2 & not ( C1 is open iff C2 is open ) ) or TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) )
assume A2: for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
( C1 is open iff C2 is open ) ; ::_thesis: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
now__::_thesis:_for_D_being_set_st_D_in_the_topology_of_X2_holds_
D_in_the_topology_of_X1
let D be set ; ::_thesis: ( D in the topology of X2 implies D in the topology of X1 )
assume A3: D in the topology of X2 ; ::_thesis: D in the topology of X1
then reconsider C2 = D as Subset of X2 ;
reconsider C1 = C2 as Subset of X1 by A1;
 C2 is open by A3, PRE_TOPC:def_2;
then  C1 is open by A2;
hence  D in the topology of X1 by PRE_TOPC:def_2; ::_thesis: verum
end;
then A4: the topology of X2 c= the topology of X1 by TARSKI:def_3;
now__::_thesis:_for_D_being_set_st_D_in_the_topology_of_X1_holds_
D_in_the_topology_of_X2
let D be set ; ::_thesis: ( D in the topology of X1 implies D in the topology of X2 )
assume A5: D in the topology of X1 ; ::_thesis: D in the topology of X2
then reconsider C1 = D as Subset of X1 ;
reconsider C2 = C1 as Subset of X2 by A1;
 C1 is open by A5, PRE_TOPC:def_2;
then  C2 is open by A2;
hence  D in the topology of X2 by PRE_TOPC:def_2; ::_thesis: verum
end;
then  the topology of X1 c= the topology of X2 by TARSKI:def_3;
hence  TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) by A1, A4, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th73: :: TOPS_3:73
for X1, X2 being TopStruct st the carrier of X1 = the carrier of X2 & ( for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
( C1 is closed iff C2 is closed ) ) holds
TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
proof
let X1, X2 be TopStruct ; ::_thesis: ( the carrier of X1 = the carrier of X2 & ( for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
( C1 is closed iff C2 is closed ) ) implies TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) )
assume A1: the carrier of X1 = the carrier of X2 ; ::_thesis: ( ex C1 being Subset of X1 ex C2 being Subset of X2 st
( C1 = C2 & not ( C1 is closed iff C2 is closed ) ) or TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) )
assume A2: for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
( C1 is closed iff C2 is closed ) ; ::_thesis: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
now__::_thesis:_for_C1_being_Subset_of_X1
for_C2_being_Subset_of_X2_st_C1_=_C2_holds_
(_(_C1_is_open_implies_C2_is_open_)_&_(_C2_is_open_implies_C1_is_open_)_)
let C1 be Subset of X1; ::_thesis: for C2 being Subset of X2 st C1 = C2 holds
( ( C1 is open implies C2 is open ) & ( C2 is open implies C1 is open ) )
let C2 be Subset of X2; ::_thesis: ( C1 = C2 implies ( ( C1 is open implies C2 is open ) & ( C2 is open implies C1 is open ) ) )
assume A3: C1 = C2 ; ::_thesis: ( ( C1 is open implies C2 is open ) & ( C2 is open implies C1 is open ) )
thus  ( C1 is open implies C2 is open ) ::_thesis: ( C2 is open implies C1 is open )
proof
assume  C1 is open ; ::_thesis: C2 is open
then  C1 ` is closed by TOPS_1:4;
then  C2 ` is closed by A1, A2, A3;
hence  C2 is open by TOPS_1:4; ::_thesis: verum
end;
thus  ( C2 is open implies C1 is open ) ::_thesis: verum
proof
assume  C2 is open ; ::_thesis: C1 is open
then  C2 ` is closed by TOPS_1:4;
then  C1 ` is closed by A1, A2, A3;
hence  C1 is open by TOPS_1:4; ::_thesis: verum
end;
end;
hence  TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) by A1, Th72; ::_thesis: verum
end;


theorem :: TOPS_3:74
for X1, X2 being TopSpace st the carrier of X1 = the carrier of X2 & ( for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
Int C1 = Int C2 ) holds
TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
proof
let X1, X2 be TopSpace; ::_thesis: ( the carrier of X1 = the carrier of X2 & ( for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
Int C1 = Int C2 ) implies TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) )
assume A1: the carrier of X1 = the carrier of X2 ; ::_thesis: ( ex C1 being Subset of X1 ex C2 being Subset of X2 st
( C1 = C2 & not Int C1 = Int C2 ) or TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) )
assume A2: for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
Int C1 = Int C2 ; ::_thesis: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
now__::_thesis:_for_C1_being_Subset_of_X1
for_C2_being_Subset_of_X2_st_C1_=_C2_holds_
(_(_C1_is_open_implies_C2_is_open_)_&_(_C2_is_open_implies_C1_is_open_)_)
let C1 be Subset of X1; ::_thesis: for C2 being Subset of X2 st C1 = C2 holds
( ( C1 is open implies C2 is open ) & ( C2 is open implies C1 is open ) )
let C2 be Subset of X2; ::_thesis: ( C1 = C2 implies ( ( C1 is open implies C2 is open ) & ( C2 is open implies C1 is open ) ) )
assume A3: C1 = C2 ; ::_thesis: ( ( C1 is open implies C2 is open ) & ( C2 is open implies C1 is open ) )
thus  ( C1 is open implies C2 is open ) ::_thesis: ( C2 is open implies C1 is open )
proof
assume  C1 is open ; ::_thesis: C2 is open
then  C1 = Int C1 by TOPS_1:23;
then  C2 = Int C2 by A2, A3;
hence  C2 is open ; ::_thesis: verum
end;
thus  ( C2 is open implies C1 is open ) ::_thesis: verum
proof
assume  C2 is open ; ::_thesis: C1 is open
then  C2 = Int C2 by TOPS_1:23;
then  C1 = Int C1 by A2, A3;
hence  C1 is open ; ::_thesis: verum
end;
end;
hence  TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) by A1, Th72; ::_thesis: verum
end;

theorem :: TOPS_3:75
for X1, X2 being TopSpace st the carrier of X1 = the carrier of X2 & ( for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
Cl C1 = Cl C2 ) holds
TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
proof
let X1, X2 be TopSpace; ::_thesis: ( the carrier of X1 = the carrier of X2 & ( for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
Cl C1 = Cl C2 ) implies TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) )
assume A1: the carrier of X1 = the carrier of X2 ; ::_thesis: ( ex C1 being Subset of X1 ex C2 being Subset of X2 st
( C1 = C2 & not Cl C1 = Cl C2 ) or TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) )
assume A2: for C1 being Subset of X1
for C2 being Subset of X2 st C1 = C2 holds
Cl C1 = Cl C2 ; ::_thesis: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)
now__::_thesis:_for_C1_being_Subset_of_X1
for_C2_being_Subset_of_X2_st_C1_=_C2_holds_
(_(_C1_is_closed_implies_C2_is_closed_)_&_(_C2_is_closed_implies_C1_is_closed_)_)
let C1 be Subset of X1; ::_thesis: for C2 being Subset of X2 st C1 = C2 holds
( ( C1 is closed implies C2 is closed ) & ( C2 is closed implies C1 is closed ) )
let C2 be Subset of X2; ::_thesis: ( C1 = C2 implies ( ( C1 is closed implies C2 is closed ) & ( C2 is closed implies C1 is closed ) ) )
assume A3: C1 = C2 ; ::_thesis: ( ( C1 is closed implies C2 is closed ) & ( C2 is closed implies C1 is closed ) )
thus  ( C1 is closed implies C2 is closed ) ::_thesis: ( C2 is closed implies C1 is closed )
proof
assume  C1 is closed ; ::_thesis: C2 is closed
then  C1 = Cl C1 by PRE_TOPC:22;
then  C2 = Cl C2 by A2, A3;
hence  C2 is closed ; ::_thesis: verum
end;
thus  ( C2 is closed implies C1 is closed ) ::_thesis: verum
proof
assume  C2 is closed ; ::_thesis: C1 is closed
then  C2 = Cl C2 by PRE_TOPC:22;
then  C1 = Cl C1 by A2, A3;
hence  C1 is closed ; ::_thesis: verum
end;
end;
hence  TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) by A1, Th73; ::_thesis: verum
end;


theorem Th76: :: TOPS_3:76
for X1, X2 being TopSpace
for D1 being Subset of X1
for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is open holds
D2 is open
proof
let X1, X2 be TopSpace; ::_thesis: for D1 being Subset of X1
for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is open holds
D2 is open
let D1 be Subset of X1; ::_thesis: for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is open holds
D2 is open
let D2 be Subset of X2; ::_thesis: ( D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is open implies D2 is open )
assume A1: D1 = D2 ; ::_thesis: ( not TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) or not D1 is open or D2 is open )
assume A2: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) ; ::_thesis: ( not D1 is open or D2 is open )
assume  D1 in the topology of X1 ; :: according to PRE_TOPC:def_2 ::_thesis: D2 is open
hence  D2 is open by A1, A2, PRE_TOPC:def_2; ::_thesis: verum
end;

theorem Th77: :: TOPS_3:77
for X1, X2 being TopSpace
for D1 being Subset of X1
for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Int D1 = Int D2
proof
let X1, X2 be TopSpace; ::_thesis: for D1 being Subset of X1
for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Int D1 = Int D2
let D1 be Subset of X1; ::_thesis: for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Int D1 = Int D2
let D2 be Subset of X2; ::_thesis: ( D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) implies Int D1 = Int D2 )
assume A1: D1 = D2 ; ::_thesis: ( not TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) or Int D1 = Int D2 )
A2: Int D1 c= D1 by TOPS_1:16;
then reconsider C2 = Int D1 as Subset of X2 by A1, XBOOLE_1:1;
assume A3: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) ; ::_thesis: Int D1 = Int D2
then A4: C2 c= Int D2 by A1, A2, Th76, TOPS_1:24;
A5: Int D2 c= D2 by TOPS_1:16;
then reconsider C1 = Int D2 as Subset of X1 by A1, XBOOLE_1:1;
 C1 c= Int D1 by A1, A3, A5, Th76, TOPS_1:24;
hence  Int D1 = Int D2 by A4, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th78: :: TOPS_3:78
for X1, X2 being TopSpace
for D1 being Subset of X1
for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Int D1 c= Int D2
proof
let X1, X2 be TopSpace; ::_thesis: for D1 being Subset of X1
for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Int D1 c= Int D2
let D1 be Subset of X1; ::_thesis: for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Int D1 c= Int D2
let D2 be Subset of X2; ::_thesis: ( D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) implies Int D1 c= Int D2 )
assume A1: D1 c= D2 ; ::_thesis: ( not TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) or Int D1 c= Int D2 )
then reconsider C2 = D1 as Subset of X2 by XBOOLE_1:1;
assume  TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) ; ::_thesis: Int D1 c= Int D2
then  Int D1 = Int C2 by Th77;
hence  Int D1 c= Int D2 by A1, TOPS_1:19; ::_thesis: verum
end;

theorem Th79: :: TOPS_3:79
for X1, X2 being TopSpace
for D1 being Subset of X1
for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is closed holds
D2 is closed
proof
let X1, X2 be TopSpace; ::_thesis: for D1 being Subset of X1
for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is closed holds
D2 is closed
let D1 be Subset of X1; ::_thesis: for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is closed holds
D2 is closed
let D2 be Subset of X2; ::_thesis: ( D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is closed implies D2 is closed )
assume A1: D1 = D2 ; ::_thesis: ( not TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) or not D1 is closed or D2 is closed )
assume A2: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) ; ::_thesis: ( not D1 is closed or D2 is closed )
assume  D1 is closed ; ::_thesis: D2 is closed
then  D2 ` is open by A1, A2, Th76;
hence  D2 is closed by TOPS_1:3; ::_thesis: verum
end;

theorem Th80: :: TOPS_3:80
for X1, X2 being TopSpace
for D1 being Subset of X1
for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Cl D1 = Cl D2
proof
let X1, X2 be TopSpace; ::_thesis: for D1 being Subset of X1
for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Cl D1 = Cl D2
let D1 be Subset of X1; ::_thesis: for D2 being Subset of X2 st D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Cl D1 = Cl D2
let D2 be Subset of X2; ::_thesis: ( D1 = D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) implies Cl D1 = Cl D2 )
assume A1: D1 = D2 ; ::_thesis: ( not TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) or Cl D1 = Cl D2 )
assume A2: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) ; ::_thesis: Cl D1 = Cl D2
then reconsider C2 = Cl D1 as Subset of X2 ;
 D1 c= Cl D1 by PRE_TOPC:18;
then A3: Cl D2 c= C2 by A1, A2, Th79, TOPS_1:5;
reconsider C1 = Cl D2 as Subset of X1 by A2;
 D2 c= Cl D2 by PRE_TOPC:18;
then  Cl D1 c= C1 by A1, A2, Th79, TOPS_1:5;
hence  Cl D1 = Cl D2 by A3, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th81: :: TOPS_3:81
for X1, X2 being TopSpace
for D1 being Subset of X1
for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Cl D1 c= Cl D2
proof
let X1, X2 be TopSpace; ::_thesis: for D1 being Subset of X1
for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Cl D1 c= Cl D2
let D1 be Subset of X1; ::_thesis: for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) holds
Cl D1 c= Cl D2
let D2 be Subset of X2; ::_thesis: ( D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) implies Cl D1 c= Cl D2 )
assume A1: D1 c= D2 ; ::_thesis: ( not TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) or Cl D1 c= Cl D2 )
assume A2: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) ; ::_thesis: Cl D1 c= Cl D2
then reconsider C2 = D1 as Subset of X2 ;
 Cl D1 = Cl C2 by A2, Th80;
hence  Cl D1 c= Cl D2 by A1, PRE_TOPC:19; ::_thesis: verum
end;

theorem Th82: :: TOPS_3:82
for X1, X2 being TopSpace
for D1 being Subset of X1
for D2 being Subset of X2 st D2 c= D1 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is boundary holds
D2 is boundary
proof
let X1, X2 be TopSpace; ::_thesis: for D1 being Subset of X1
for D2 being Subset of X2 st D2 c= D1 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is boundary holds
D2 is boundary
let D1 be Subset of X1; ::_thesis: for D2 being Subset of X2 st D2 c= D1 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is boundary holds
D2 is boundary
let D2 be Subset of X2; ::_thesis: ( D2 c= D1 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is boundary implies D2 is boundary )
assume A1: D2 c= D1 ; ::_thesis: ( not TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) or not D1 is boundary or D2 is boundary )
then reconsider C1 = D2 as Subset of X1 by XBOOLE_1:1;
assume A2: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) ; ::_thesis: ( not D1 is boundary or D2 is boundary )
assume  D1 is boundary ; ::_thesis: D2 is boundary
then  C1 is boundary by A1, Th11;
then A3: Int C1 = {} ;
 Int C1 = Int D2 by A2, Th77;
hence  D2 is boundary by A3, Def1; ::_thesis: verum
end;

theorem Th83: :: TOPS_3:83
for X1, X2 being TopSpace
for D1 being Subset of X1
for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is dense holds
D2 is dense
proof
let X1, X2 be TopSpace; ::_thesis: for D1 being Subset of X1
for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is dense holds
D2 is dense
let D1 be Subset of X1; ::_thesis: for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is dense holds
D2 is dense
let D2 be Subset of X2; ::_thesis: ( D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is dense implies D2 is dense )
assume A1: D1 c= D2 ; ::_thesis: ( not TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) or not D1 is dense or D2 is dense )
then reconsider C2 = D1 as Subset of X2 by XBOOLE_1:1;
assume A2: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) ; ::_thesis: ( not D1 is dense or D2 is dense )
assume  D1 is dense ; ::_thesis: D2 is dense
then A3: Cl D1 = the carrier of X1 by Def2;
 Cl D1 = Cl C2 by A2, Th80;
then  C2 is dense by A2, A3, Def2;
hence  D2 is dense by A1, TOPS_1:44; ::_thesis: verum
end;

theorem :: TOPS_3:84
for X1, X2 being TopSpace
for D1 being Subset of X1
for D2 being Subset of X2 st D2 c= D1 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is nowhere_dense holds
D2 is nowhere_dense
proof
let X1, X2 be TopSpace; ::_thesis: for D1 being Subset of X1
for D2 being Subset of X2 st D2 c= D1 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is nowhere_dense holds
D2 is nowhere_dense
let D1 be Subset of X1; ::_thesis: for D2 being Subset of X2 st D2 c= D1 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is nowhere_dense holds
D2 is nowhere_dense
let D2 be Subset of X2; ::_thesis: ( D2 c= D1 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is nowhere_dense implies D2 is nowhere_dense )
assume A1: D2 c= D1 ; ::_thesis: ( not TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) or not D1 is nowhere_dense or D2 is nowhere_dense )
assume A2: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) ; ::_thesis: ( not D1 is nowhere_dense or D2 is nowhere_dense )
assume  D1 is nowhere_dense ; ::_thesis: D2 is nowhere_dense
then  Cl D1 is boundary by TOPS_1:def_5;
then  Cl D2 is boundary by A1, A2, Th81, Th82;
hence  D2 is nowhere_dense by TOPS_1:def_5; ::_thesis: verum
end;


theorem :: TOPS_3:85
for X1, X2 being non empty TopSpace
for D1 being Subset of X1
for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is everywhere_dense holds
D2 is everywhere_dense
proof
let X1, X2 be non empty TopSpace; ::_thesis: for D1 being Subset of X1
for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is everywhere_dense holds
D2 is everywhere_dense
let D1 be Subset of X1; ::_thesis: for D2 being Subset of X2 st D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is everywhere_dense holds
D2 is everywhere_dense
let D2 be Subset of X2; ::_thesis: ( D1 c= D2 & TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) & D1 is everywhere_dense implies D2 is everywhere_dense )
assume A1: D1 c= D2 ; ::_thesis: ( not TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) or not D1 is everywhere_dense or D2 is everywhere_dense )
assume A2: TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #) ; ::_thesis: ( not D1 is everywhere_dense or D2 is everywhere_dense )
assume  D1 is everywhere_dense ; ::_thesis: D2 is everywhere_dense
then  Int D1 is dense by Th35;
then  Int D2 is dense by A1, A2, Th78, Th83;
hence  D2 is everywhere_dense by Th35; ::_thesis: verum
end;