:: TOPS_1 semantic presentation

begin


theorem :: TOPS_1:1
for TS being 1-sorted
for K, Q being Subset of TS st K ` = Q ` holds
K = Q by SUBSET_1:42;


theorem Th2: :: TOPS_1:2
for GX being TopStruct holds Cl ([#] GX) = [#] GX
proof
let GX be TopStruct ; ::_thesis: Cl ([#] GX) = [#] GX
thus  Cl ([#] GX) c= [#] GX ; :: according to XBOOLE_0:def_10 ::_thesis: [#] GX c= Cl ([#] GX)
thus  [#] GX c= Cl ([#] GX) by PRE_TOPC:18; ::_thesis: verum
end;

registration
let T be TopSpace;
let P be Subset of T;
cluster Cl P ->  closed ;
coherence
 Cl P is closed
proof
 Cl (Cl P) = Cl P ;
hence  Cl P is closed by PRE_TOPC:22; ::_thesis: verum
end;
end;

theorem Th3: :: TOPS_1:3
for GX being TopStruct
for R being Subset of GX holds
( R is closed iff R ` is open )
proof
let GX be TopStruct ; ::_thesis: for R being Subset of GX holds
( R is closed iff R ` is open )
let R be Subset of GX; ::_thesis: ( R is closed iff R ` is open )
 ( R is closed iff ([#] GX) \ R is open ) by PRE_TOPC:def_3;
hence  ( R is closed iff R ` is open ) ; ::_thesis: verum
end;

registration
let T be TopSpace;
let R be closed Subset of T;
clusterR `  ->  open ;
coherence
 R ` is open by Th3;
end;

theorem Th4: :: TOPS_1:4
for GX being TopStruct
for R being Subset of GX holds
( R is open iff R ` is closed )
proof
let GX be TopStruct ; ::_thesis: for R being Subset of GX holds
( R is open iff R ` is closed )
let R be Subset of GX; ::_thesis: ( R is open iff R ` is closed )
 ( R ` is closed iff (R `) ` is open ) by Th3;
hence  ( R is open iff R ` is closed ) ; ::_thesis: verum
end;

registration
let T be TopSpace;
cluster open for Element of K10( the carrier of T);
existence
 ex b1 being Subset of T st b1 is open
proof
take  ({} T) ` ; ::_thesis: ({} T) ` is open
thus  ({} T) ` is open ; ::_thesis: verum
end;
end;

registration
let T be TopSpace;
let R be open Subset of T;
clusterR `  ->  closed ;
coherence
 R ` is closed by Th4;
end;

theorem :: TOPS_1:5
for GX being TopStruct
for S, T being Subset of GX st S is closed & T c= S holds
Cl T c= S
proof
let GX be TopStruct ; ::_thesis: for S, T being Subset of GX st S is closed & T c= S holds
Cl T c= S
let S, T be Subset of GX; ::_thesis: ( S is closed & T c= S implies Cl T c= S )
assume that
A1: S is closed and
A2: T c= S ; ::_thesis: Cl T c= S
 Cl S = S by A1, PRE_TOPC:22;
hence  Cl T c= S by A2, PRE_TOPC:19; ::_thesis: verum
end;

theorem Th6: :: TOPS_1:6
for TS being TopSpace
for K, L being Subset of TS holds (Cl K) \ (Cl L) c= Cl (K \ L)
proof
let TS be TopSpace; ::_thesis: for K, L being Subset of TS holds (Cl K) \ (Cl L) c= Cl (K \ L)
let K, L be Subset of TS; ::_thesis: (Cl K) \ (Cl L) c= Cl (K \ L)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Cl K) \ (Cl L) or x in Cl (K \ L) )
(Cl K) \/ (Cl L) = Cl (K \/ L) by PRE_TOPC:20
.= Cl ((K \ L) \/ L) by XBOOLE_1:39
.= (Cl (K \ L)) \/ (Cl L) by PRE_TOPC:20 ;
then A1: ( x in (Cl K) \/ (Cl L) iff ( x in Cl (K \ L) or x in Cl L ) ) by XBOOLE_0:def_3;
assume A2: x in (Cl K) \ (Cl L) ; ::_thesis: x in Cl (K \ L)
then  x in Cl K by XBOOLE_0:def_5;
hence  x in Cl (K \ L) by A2, A1, XBOOLE_0:def_3, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem Th7: :: TOPS_1:7
for GX being TopStruct
for R, S being Subset of GX st R is closed & S is closed holds
Cl (R /\ S) = (Cl R) /\ (Cl S)
proof
let GX be TopStruct ; ::_thesis: for R, S being Subset of GX st R is closed & S is closed holds
Cl (R /\ S) = (Cl R) /\ (Cl S)
let R, S be Subset of GX; ::_thesis: ( R is closed & S is closed implies Cl (R /\ S) = (Cl R) /\ (Cl S) )
assume that
A1: R is closed and
A2: S is closed ; ::_thesis: Cl (R /\ S) = (Cl R) /\ (Cl S)
A3: S = Cl S by A2, PRE_TOPC:22;
A4: Cl (R /\ S) c= (Cl R) /\ (Cl S) by PRE_TOPC:21;
 R = Cl R by A1, PRE_TOPC:22;
then  (Cl R) /\ (Cl S) c= Cl (R /\ S) by A3, PRE_TOPC:18;
hence  Cl (R /\ S) = (Cl R) /\ (Cl S) by A4, XBOOLE_0:def_10; ::_thesis: verum
end;

registration
let TS be TopSpace;
let P, Q be closed Subset of TS;
clusterP /\ Q ->  closed for Subset of TS;
coherence
 for b1 being Subset of TS st b1 = P /\ Q holds
b1 is closed
proof
A1: Q = Cl Q by PRE_TOPC:22;
 P = Cl P by PRE_TOPC:22;
then  Cl (P /\ Q) = P /\ Q by A1, Th7;
hence  for b1 being Subset of TS st b1 = P /\ Q holds
b1 is closed ; ::_thesis: verum
end;
clusterP \/ Q ->  closed for Subset of TS;
coherence
 for b1 being Subset of TS st b1 = P \/ Q holds
b1 is closed
proof
A2: Q = Cl Q by PRE_TOPC:22;
 P = Cl P by PRE_TOPC:22;
then  Cl (P \/ Q) = P \/ Q by A2, PRE_TOPC:20;
hence  for b1 being Subset of TS st b1 = P \/ Q holds
b1 is closed ; ::_thesis: verum
end;
end;

theorem :: TOPS_1:8
for TS being TopSpace
for P, Q being Subset of TS st P is closed & Q is closed holds
P /\ Q is closed ;

theorem :: TOPS_1:9
for TS being TopSpace
for P, Q being Subset of TS st P is closed & Q is closed holds
P \/ Q is closed ;

registration
let TS be TopSpace;
let P, Q be open Subset of TS;
clusterP /\ Q ->  open for Subset of TS;
coherence
 for b1 being Subset of TS st b1 = P /\ Q holds
b1 is open
proof
 (P `) \/ (Q `) = (P /\ Q) ` by XBOOLE_1:54;
hence  for b1 being Subset of TS st b1 = P /\ Q holds
b1 is open by Th4; ::_thesis: verum
end;
clusterP \/ Q ->  open for Subset of TS;
coherence
 for b1 being Subset of TS st b1 = P \/ Q holds
b1 is open
proof
 (P `) /\ (Q `) = (P \/ Q) ` by XBOOLE_1:53;
hence  for b1 being Subset of TS st b1 = P \/ Q holds
b1 is open by Th4; ::_thesis: verum
end;
end;

theorem :: TOPS_1:10
for TS being TopSpace
for P, Q being Subset of TS st P is open & Q is open holds
P \/ Q is open ;

theorem :: TOPS_1:11
for TS being TopSpace
for P, Q being Subset of TS st P is open & Q is open holds
P /\ Q is open ;

theorem Th12: :: TOPS_1:12
for GX being non empty TopSpace
for R being Subset of GX
for p being Point of GX holds
( p in Cl R iff for T being Subset of GX st T is open & p in T holds
R meets T )
proof
let GX be non empty TopSpace; ::_thesis: for R being Subset of GX
for p being Point of GX holds
( p in Cl R iff for T being Subset of GX st T is open & p in T holds
R meets T )
let R be Subset of GX; ::_thesis: for p being Point of GX holds
( p in Cl R iff for T being Subset of GX st T is open & p in T holds
R meets T )
let p be Point of GX; ::_thesis: ( p in Cl R iff for T being Subset of GX st T is open & p in T holds
R meets T )
hereby  ::_thesis: ( ( for T being Subset of GX st T is open & p in T holds
R meets T ) implies p in Cl R )
assume A1: p in Cl R ; ::_thesis: for T being Subset of GX holds
( not T is open or not p in T or not R misses T )
given T being Subset of GX such that A2: T is open and
A3: p in T and
A4: R misses T ; ::_thesis: contradiction
A5: (R `) \/ (T `) = (R /\ T) ` by XBOOLE_1:54;
A6: R /\ T = {} GX by A4, XBOOLE_0:def_7;
A7: R c= T `
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R or x in T ` )
assume A8: x in R ; ::_thesis: x in T `
then  ( x in R ` or x in T ` ) by A5, A6, XBOOLE_0:def_3;
hence  x in T ` by A8, XBOOLE_0:def_5; ::_thesis: verum
end;
 Cl (T `) = T ` by A2, PRE_TOPC:22;
then  Cl R c= T ` by A7, PRE_TOPC:19;
hence  contradiction by A1, A3, XBOOLE_0:def_5; ::_thesis: verum
end;
assume A9: for T being Subset of GX st T is open & p in T holds
R meets T ; ::_thesis: p in Cl R
assume  not p in Cl R ; ::_thesis: contradiction
then  p in (Cl R) ` by SUBSET_1:29;
then A10: R meets (Cl R) ` by A9;
 R misses R ` by XBOOLE_1:79;
then A11: R /\ (R `) = {} by XBOOLE_0:def_7;
 R c= Cl R by PRE_TOPC:18;
then  (Cl R) ` c= R ` by SUBSET_1:12;
then  R /\ ((Cl R) `) = {} by A11, XBOOLE_1:3, XBOOLE_1:26;
hence  contradiction by A10, XBOOLE_0:def_7; ::_thesis: verum
end;

theorem Th13: :: TOPS_1:13
for TS being TopSpace
for Q, K being Subset of TS st Q is open holds
Q /\ (Cl K) c= Cl (Q /\ K)
proof
let TS be TopSpace; ::_thesis: for Q, K being Subset of TS st Q is open holds
Q /\ (Cl K) c= Cl (Q /\ K)
let Q, K be Subset of TS; ::_thesis: ( Q is open implies Q /\ (Cl K) c= Cl (Q /\ K) )
assume A1: Q is open ; ::_thesis: Q /\ (Cl K) c= Cl (Q /\ K)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q /\ (Cl K) or x in Cl (Q /\ K) )
assume A2: x in Q /\ (Cl K) ; ::_thesis: x in Cl (Q /\ K)
then A3: x in Cl K by XBOOLE_0:def_4;
reconsider p99 = x as Point of TS by A2;
A4: not TS is empty by A2;
A5: x in Q by A2, XBOOLE_0:def_4;
 for Q1 being Subset of TS st Q1 is open & p99 in Q1 holds
Q /\ K meets Q1
proof
let Q1 be Subset of TS; ::_thesis: ( Q1 is open & p99 in Q1 implies Q /\ K meets Q1 )
assume A6: Q1 is open ; ::_thesis: ( not p99 in Q1 or Q /\ K meets Q1 )
assume  p99 in Q1 ; ::_thesis: Q /\ K meets Q1
then  p99 in Q1 /\ Q by A5, XBOOLE_0:def_4;
then  K meets Q1 /\ Q by A1, A3, A4, A6, Th12;
then A7: K /\ (Q1 /\ Q) <> {} by XBOOLE_0:def_7;
 K /\ (Q1 /\ Q) = (Q /\ K) /\ Q1 by XBOOLE_1:16;
hence  Q /\ K meets Q1 by A7, XBOOLE_0:def_7; ::_thesis: verum
end;
hence  x in Cl (Q /\ K) by A4, Th12; ::_thesis: verum
end;

theorem :: TOPS_1:14
for TS being TopSpace
for Q, K being Subset of TS st Q is open holds
Cl (Q /\ (Cl K)) = Cl (Q /\ K)
proof
let TS be TopSpace; ::_thesis: for Q, K being Subset of TS st Q is open holds
Cl (Q /\ (Cl K)) = Cl (Q /\ K)
let Q, K be Subset of TS; ::_thesis: ( Q is open implies Cl (Q /\ (Cl K)) = Cl (Q /\ K) )
A1: Cl (Q /\ K) c= Cl (Q /\ (Cl K))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl (Q /\ K) or x in Cl (Q /\ (Cl K)) )
assume A2: x in Cl (Q /\ K) ; ::_thesis: x in Cl (Q /\ (Cl K))
then reconsider p99 = x as Point of TS ;
A3: not TS is empty by A2;
 for Q1 being Subset of TS st Q1 is open & p99 in Q1 holds
Q /\ (Cl K) meets Q1
proof
let Q1 be Subset of TS; ::_thesis: ( Q1 is open & p99 in Q1 implies Q /\ (Cl K) meets Q1 )
assume A4: Q1 is open ; ::_thesis: ( not p99 in Q1 or Q /\ (Cl K) meets Q1 )
assume  p99 in Q1 ; ::_thesis: Q /\ (Cl K) meets Q1
then  Q /\ K meets Q1 by A2, A3, A4, Th12;
then A5: (Q /\ K) /\ Q1 <> {} by XBOOLE_0:def_7;
 Q /\ K c= Q /\ (Cl K) by PRE_TOPC:18, XBOOLE_1:26;
then  (Q /\ (Cl K)) /\ Q1 <> {} by A5, XBOOLE_1:3, XBOOLE_1:26;
hence  Q /\ (Cl K) meets Q1 by XBOOLE_0:def_7; ::_thesis: verum
end;
hence  x in Cl (Q /\ (Cl K)) by A3, Th12; ::_thesis: verum
end;
assume  Q is open ; ::_thesis: Cl (Q /\ (Cl K)) = Cl (Q /\ K)
then  Cl (Q /\ (Cl K)) c= Cl (Cl (Q /\ K)) by Th13, PRE_TOPC:19;
hence  Cl (Q /\ (Cl K)) = Cl (Q /\ K) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

definition
let GX be TopStruct ;
let R be Subset of GX;
func Int R ->  Subset of GX equals :: TOPS_1:def 1
(Cl (R `)) ` ;
coherence
 (Cl (R `)) ` is Subset of GX ;
projectivity
 for b1, b2 being Subset of GX st b1 = (Cl (b2 `)) ` holds
b1 = (Cl (b1 `)) ` ;
end;

:: deftheorem  defines Int TOPS_1:def_1_:_
 for GX being TopStruct
for R being Subset of GX holds Int R = (Cl (R `)) ` ;

theorem Th15: :: TOPS_1:15
for TS being TopSpace holds Int ([#] TS) = [#] TS
proof
let TS be TopSpace; ::_thesis: Int ([#] TS) = [#] TS
 Int ([#] TS) = ({} TS) ` by PRE_TOPC:22;
hence  Int ([#] TS) = [#] TS ; ::_thesis: verum
end;

theorem Th16: :: TOPS_1:16
for GX being TopStruct
for T being Subset of GX holds Int T c= T
proof
let GX be TopStruct ; ::_thesis: for T being Subset of GX holds Int T c= T
let T be Subset of GX; ::_thesis: Int T c= T
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Int T or x in T )
assume A1: x in Int T ; ::_thesis: x in T
then reconsider x99 = x as Point of GX ;
 T ` c= Cl (T `) by PRE_TOPC:18;
then  not x99 in T ` by A1, XBOOLE_0:def_5;
hence  x in T by A1, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem Th17: :: TOPS_1:17
for TS being TopSpace
for K, L being Subset of TS holds (Int K) /\ (Int L) = Int (K /\ L)
proof
let TS be TopSpace; ::_thesis: for K, L being Subset of TS holds (Int K) /\ (Int L) = Int (K /\ L)
let K, L be Subset of TS; ::_thesis: (Int K) /\ (Int L) = Int (K /\ L)
(Int K) /\ (Int L) = ((Cl (K `)) \/ (Cl (L `))) ` by XBOOLE_1:53
.= (Cl ((K `) \/ (L `))) ` by PRE_TOPC:20
.= (Cl ((K /\ L) `)) ` by XBOOLE_1:54 ;
hence  (Int K) /\ (Int L) = Int (K /\ L) ; ::_thesis: verum
end;

registration
let GX be TopStruct ;
cluster Int ({} GX) ->  empty ;
coherence
 Int ({} GX) is empty
proof
{} GX = ([#] GX) ` by XBOOLE_1:37
.= (Cl (({} GX) `)) ` by Th2 ;
hence  Int ({} GX) is empty ; ::_thesis: verum
end;
end;

theorem :: TOPS_1:18
for GX being TopStruct holds Int ({} GX) = {} GX ;

theorem Th19: :: TOPS_1:19
for GX being TopStruct
for T, W being Subset of GX st T c= W holds
Int T c= Int W
proof
let GX be TopStruct ; ::_thesis: for T, W being Subset of GX st T c= W holds
Int T c= Int W
let T, W be Subset of GX; ::_thesis: ( T c= W implies Int T c= Int W )
assume  T c= W ; ::_thesis: Int T c= Int W
then  W ` c= T ` by SUBSET_1:12;
then  Cl (W `) c= Cl (T `) by PRE_TOPC:19;
hence  Int T c= Int W by SUBSET_1:12; ::_thesis: verum
end;

theorem Th20: :: TOPS_1:20
for GX being TopStruct
for T, W being Subset of GX holds (Int T) \/ (Int W) c= Int (T \/ W)
proof
let GX be TopStruct ; ::_thesis: for T, W being Subset of GX holds (Int T) \/ (Int W) c= Int (T \/ W)
let T, W be Subset of GX; ::_thesis: (Int T) \/ (Int W) c= Int (T \/ W)
A1: Cl ((T `) /\ (W `)) c= (Cl (T `)) /\ (Cl (W `)) by PRE_TOPC:21;
 (Int T) \/ (Int W) = ((Cl (T `)) /\ (Cl (W `))) ` by XBOOLE_1:54;
then  (Int T) \/ (Int W) c= (Cl ((T `) /\ (W `))) ` by A1, SUBSET_1:12;
hence  (Int T) \/ (Int W) c= Int (T \/ W) by XBOOLE_1:53; ::_thesis: verum
end;

theorem :: TOPS_1:21
for TS being TopSpace
for K, L being Subset of TS holds Int (K \ L) c= (Int K) \ (Int L)
proof
let TS be TopSpace; ::_thesis: for K, L being Subset of TS holds Int (K \ L) c= (Int K) \ (Int L)
let K, L be Subset of TS; ::_thesis: Int (K \ L) c= (Int K) \ (Int L)
A1: Int (K \ L) = (Cl ((K /\ (L `)) `)) ` by SUBSET_1:13
.= (Cl ((K `) \/ ((L `) `))) ` by XBOOLE_1:54
.= ((Cl (K `)) \/ (Cl L)) ` by PRE_TOPC:20
.= ((Cl L) `) /\ (Int K) by XBOOLE_1:53 ;
 L c= Cl L by PRE_TOPC:18;
then A2: (Cl L) ` c= L ` by SUBSET_1:12;
 Int L c= L by Th16;
then  L ` c= (Int L) ` by SUBSET_1:12;
then  (Cl L) ` c= (Int L) ` by A2, XBOOLE_1:1;
then  Int (K \ L) c= (Int K) /\ ((Int L) `) by A1, XBOOLE_1:26;
hence  Int (K \ L) c= (Int K) \ (Int L) by SUBSET_1:13; ::_thesis: verum
end;

registration
let T be TopSpace;
let K be Subset of T;
cluster Int K ->  open ;
coherence
 Int K is open ;
end;

registration
let T be TopSpace;
cluster empty  ->  open for Element of K10( the carrier of T);
coherence
 for b1 being Subset of T st b1 is empty holds
b1 is open
proof
let S be Subset of T; ::_thesis: ( S is empty implies S is open )
 Int ({} T) = {} T ;
hence  ( S is empty implies S is open ) ; ::_thesis: verum
end;
cluster [#] T ->  open ;
coherence
 [#] T is open
proof
 Int ([#] T) = [#] T by Th15;
hence  [#] T is open ; ::_thesis: verum
end;
end;

registration
let T be TopSpace;
cluster open closed for Element of K10( the carrier of T);
existence
 ex b1 being Subset of T st
( b1 is open & b1 is closed )
proof
take  [#] T ; ::_thesis: ( [#] T is open & [#] T is closed )
thus  ( [#] T is open & [#] T is closed ) ; ::_thesis: verum
end;
end;

registration
let T be non empty TopSpace;
cluster non empty open closed for Element of K10( the carrier of T);
existence
 ex b1 being Subset of T st
( not b1 is empty & b1 is open & b1 is closed )
proof
take  [#] T ; ::_thesis: ( not [#] T is empty & [#] T is open & [#] T is closed )
thus  ( not [#] T is empty & [#] T is open & [#] T is closed ) ; ::_thesis: verum
end;
end;

theorem Th22: :: TOPS_1:22
for TS being TopSpace
for x being set
for K being Subset of TS holds
( x in Int K iff ex Q being Subset of TS st
( Q is open & Q c= K & x in Q ) )
proof
let TS be TopSpace; ::_thesis: for x being set
for K being Subset of TS holds
( x in Int K iff ex Q being Subset of TS st
( Q is open & Q c= K & x in Q ) )
let x be set ; ::_thesis: for K being Subset of TS holds
( x in Int K iff ex Q being Subset of TS st
( Q is open & Q c= K & x in Q ) )
let K be Subset of TS; ::_thesis: ( x in Int K iff ex Q being Subset of TS st
( Q is open & Q c= K & x in Q ) )
thus  ( x in Int K implies ex Q being Subset of TS st
( Q is open & Q c= K & x in Q ) ) by Th16; ::_thesis: ( ex Q being Subset of TS st
( Q is open & Q c= K & x in Q ) implies x in Int K )
given Q being Subset of TS such that A1: Q is open and
A2: Q c= K and
A3: x in Q ; ::_thesis: x in Int K
 K ` c= Q ` by A2, SUBSET_1:12;
then  Cl (K `) c= Cl (Q `) by PRE_TOPC:19;
then  Cl (K `) c= Q ` by A1, PRE_TOPC:22;
then  (Q `) ` c= (Cl (K `)) ` by SUBSET_1:12;
hence  x in Int K by A3; ::_thesis: verum
end;

theorem Th23: :: TOPS_1:23
for TS being TopSpace
for GX being TopStruct
for P being Subset of TS
for R being Subset of GX holds
( ( R is open implies Int R = R ) & ( Int P = P implies P is open ) )
proof
let TS be TopSpace; ::_thesis: for GX being TopStruct
for P being Subset of TS
for R being Subset of GX holds
( ( R is open implies Int R = R ) & ( Int P = P implies P is open ) )
let GX be TopStruct ; ::_thesis: for P being Subset of TS
for R being Subset of GX holds
( ( R is open implies Int R = R ) & ( Int P = P implies P is open ) )
let P be Subset of TS; ::_thesis: for R being Subset of GX holds
( ( R is open implies Int R = R ) & ( Int P = P implies P is open ) )
let R be Subset of GX; ::_thesis: ( ( R is open implies Int R = R ) & ( Int P = P implies P is open ) )
hereby  ::_thesis: ( Int P = P implies P is open )
assume  R is open ; ::_thesis: Int R = R
then  R ` is closed by Th4;
then  Cl (R `) = R ` by PRE_TOPC:22;
hence  Int R = R ; ::_thesis: verum
end;
thus  ( Int P = P implies P is open ) ; ::_thesis: verum
end;

theorem :: TOPS_1:24
for GX being TopStruct
for S, T being Subset of GX st S is open & S c= T holds
S c= Int T
proof
let GX be TopStruct ; ::_thesis: for S, T being Subset of GX st S is open & S c= T holds
S c= Int T
let S, T be Subset of GX; ::_thesis: ( S is open & S c= T implies S c= Int T )
assume that
A1: S is open and
A2: S c= T ; ::_thesis: S c= Int T
 Int S = S by A1, Th23;
hence  S c= Int T by A2, Th19; ::_thesis: verum
end;

theorem :: TOPS_1:25
for TS being TopSpace
for P being Subset of TS holds
( P is open iff for x being set holds
( x in P iff ex Q being Subset of TS st
( Q is open & Q c= P & x in Q ) ) )
proof
let TS be TopSpace; ::_thesis: for P being Subset of TS holds
( P is open iff for x being set holds
( x in P iff ex Q being Subset of TS st
( Q is open & Q c= P & x in Q ) ) )
let P be Subset of TS; ::_thesis: ( P is open iff for x being set holds
( x in P iff ex Q being Subset of TS st
( Q is open & Q c= P & x in Q ) ) )
thus  ( P is open implies for x being set holds
( x in P iff ex Q being Subset of TS st
( Q is open & Q c= P & x in Q ) ) ) ; ::_thesis: ( ( for x being set holds
( x in P iff ex Q being Subset of TS st
( Q is open & Q c= P & x in Q ) ) ) implies P is open )
assume A1: for x being set holds
( x in P iff ex Q being Subset of TS st
( Q is open & Q c= P & x in Q ) ) ; ::_thesis: P is open
now__::_thesis:_for_x_being_set_holds_
(_x_in_P_iff_x_in_Int_P_)
let x be set ; ::_thesis: ( x in P iff x in Int P )
 ( x in P iff ex Q being Subset of TS st
( Q is open & Q c= P & x in Q ) ) by A1;
hence  ( x in P iff x in Int P ) by Th22; ::_thesis: verum
end;
hence  P is open by TARSKI:1; ::_thesis: verum
end;

theorem Th26: :: TOPS_1:26
for GX being TopStruct
for T being Subset of GX holds Cl (Int T) = Cl (Int (Cl (Int T)))
proof
let GX be TopStruct ; ::_thesis: for T being Subset of GX holds Cl (Int T) = Cl (Int (Cl (Int T)))
let T be Subset of GX; ::_thesis: Cl (Int T) = Cl (Int (Cl (Int T)))
 Int (Int T) c= Int (Cl (Int T)) by Th19, PRE_TOPC:18;
then A1: Cl (Int T) c= Cl (Int (Cl (Int T))) by PRE_TOPC:19;
 Cl (Int (Cl (Int T))) c= Cl (Cl (Int T)) by Th16, PRE_TOPC:19;
hence  Cl (Int T) = Cl (Int (Cl (Int T))) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: TOPS_1:27
for GX being TopStruct
for R being Subset of GX st R is open holds
Cl (Int (Cl R)) = Cl R
proof
let GX be TopStruct ; ::_thesis: for R being Subset of GX st R is open holds
Cl (Int (Cl R)) = Cl R
let R be Subset of GX; ::_thesis: ( R is open implies Cl (Int (Cl R)) = Cl R )
assume A1: R is open ; ::_thesis: Cl (Int (Cl R)) = Cl R
then  Cl (Int (Cl R)) = Cl (Int (Cl (Int R))) by Th23
.= Cl (Int R) by Th26
.= Cl R by A1, Th23 ;
hence  Cl (Int (Cl R)) = Cl R ; ::_thesis: verum
end;

definition
let GX be TopStruct ;
let R be Subset of GX;
func Fr R ->  Subset of GX equals :: TOPS_1:def 2
(Cl R) /\ (Cl (R `));
coherence
 (Cl R) /\ (Cl (R `)) is Subset of GX ;
end;

:: deftheorem  defines Fr TOPS_1:def_2_:_
 for GX being TopStruct
for R being Subset of GX holds Fr R = (Cl R) /\ (Cl (R `));

registration
let T be TopSpace;
let A be Subset of T;
cluster Fr A ->  closed ;
coherence
 Fr A is closed ;
end;

theorem Th28: :: TOPS_1:28
for GX being non empty TopSpace
for R being Subset of GX
for p being Point of GX holds
( p in Fr R iff for S being Subset of GX st S is open & p in S holds
( R meets S & R ` meets S ) )
proof
let GX be non empty TopSpace; ::_thesis: for R being Subset of GX
for p being Point of GX holds
( p in Fr R iff for S being Subset of GX st S is open & p in S holds
( R meets S & R ` meets S ) )
let R be Subset of GX; ::_thesis: for p being Point of GX holds
( p in Fr R iff for S being Subset of GX st S is open & p in S holds
( R meets S & R ` meets S ) )
let p be Point of GX; ::_thesis: ( p in Fr R iff for S being Subset of GX st S is open & p in S holds
( R meets S & R ` meets S ) )
hereby  ::_thesis: ( ( for S being Subset of GX st S is open & p in S holds
( R meets S & R ` meets S ) ) implies p in Fr R )
assume A1: p in Fr R ; ::_thesis: for S being Subset of GX st S is open & p in S holds
( R meets S & R ` meets S )
then A2: p in Cl (R `) by XBOOLE_0:def_4;
let S be Subset of GX; ::_thesis: ( S is open & p in S implies ( R meets S & R ` meets S ) )
assume that
A3: S is open and
A4: p in S ; ::_thesis: ( R meets S & R ` meets S )
 p in Cl R by A1, XBOOLE_0:def_4;
hence  ( R meets S & R ` meets S ) by A3, A4, A2, Th12; ::_thesis: verum
end;
assume A5: for S being Subset of GX st S is open & p in S holds
( R meets S & R ` meets S ) ; ::_thesis: p in Fr R
then  for S being Subset of GX st S is open & p in S holds
R ` meets S ;
then A6: p in Cl (R `) by Th12;
 for S being Subset of GX st S is open & p in S holds
R meets S by A5;
then  p in Cl R by Th12;
hence  p in Fr R by A6, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem :: TOPS_1:29
for GX being TopStruct
for T being Subset of GX holds Fr T = Fr (T `) ;

theorem :: TOPS_1:30
for GX being TopStruct
for T being Subset of GX holds Fr T = ((Cl (T `)) /\ T) \/ ((Cl T) \ T)
proof
let GX be TopStruct ; ::_thesis: for T being Subset of GX holds Fr T = ((Cl (T `)) /\ T) \/ ((Cl T) \ T)
let T be Subset of GX; ::_thesis: Fr T = ((Cl (T `)) /\ T) \/ ((Cl T) \ T)
 for x being set holds
( x in Fr T iff x in ((Cl (T `)) /\ T) \/ ((Cl T) \ T) )
proof
let x be set ; ::_thesis: ( x in Fr T iff x in ((Cl (T `)) /\ T) \/ ((Cl T) \ T) )
A1: T ` c= Cl (T `) by PRE_TOPC:18;
thus  ( x in Fr T implies x in ((Cl (T `)) /\ T) \/ ((Cl T) \ T) ) ::_thesis: ( x in ((Cl (T `)) /\ T) \/ ((Cl T) \ T) implies x in Fr T )
proof
assume A2: x in Fr T ; ::_thesis: x in ((Cl (T `)) /\ T) \/ ((Cl T) \ T)
then reconsider x99 = x as Point of GX ;
 ( ( x99 in Cl T & x99 in Cl (T `) & x99 in T ) or ( x99 in Cl T & x99 in Cl (T `) & x99 in T ` ) ) by A2, SUBSET_1:29, XBOOLE_0:def_4;
then  ( x99 in (Cl (T `)) /\ T or ( not x99 in T & x99 in Cl T ) ) by XBOOLE_0:def_4;
then  ( x99 in (Cl (T `)) /\ T or x99 in (Cl T) \ T ) by XBOOLE_0:def_5;
hence  x in ((Cl (T `)) /\ T) \/ ((Cl T) \ T) by XBOOLE_0:def_3; ::_thesis: verum
end;
A3: T c= Cl T by PRE_TOPC:18;
thus  ( x in ((Cl (T `)) /\ T) \/ ((Cl T) \ T) implies x in Fr T ) ::_thesis: verum
proof
assume A4: x in ((Cl (T `)) /\ T) \/ ((Cl T) \ T) ; ::_thesis: x in Fr T
then reconsider x99 = x as Point of GX ;
 ( x99 in (Cl (T `)) /\ T or x99 in (Cl T) \ T ) by A4, XBOOLE_0:def_3;
then  ( ( x99 in Cl (T `) & x99 in T ) or ( x99 in Cl T & not x99 in T ) ) by XBOOLE_0:def_4, XBOOLE_0:def_5;
then  ( ( x99 in Cl (T `) & x99 in T ) or ( x99 in Cl T & x99 in T ` ) ) by SUBSET_1:29;
hence  x in Fr T by A3, A1, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
hence  Fr T = ((Cl (T `)) /\ T) \/ ((Cl T) \ T) by TARSKI:1; ::_thesis: verum
end;

theorem Th31: :: TOPS_1:31
for GX being TopStruct
for T being Subset of GX holds Cl T = T \/ (Fr T)
proof
let GX be TopStruct ; ::_thesis: for T being Subset of GX holds Cl T = T \/ (Fr T)
let T be Subset of GX; ::_thesis: Cl T = T \/ (Fr T)
A1: (T \/ (Cl T)) /\ (T \/ (Cl (T `))) = (Cl T) /\ (T \/ (Cl (T `))) by PRE_TOPC:18, XBOOLE_1:12;
 T \/ ((Cl T) \ T) c= T \/ ((Cl T) /\ (Cl (T `)))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in T \/ ((Cl T) \ T) or x in T \/ ((Cl T) /\ (Cl (T `))) )
assume A2: x in T \/ ((Cl T) \ T) ; ::_thesis: x in T \/ ((Cl T) /\ (Cl (T `)))
then reconsider x99 = x as Point of GX ;
 ( x99 in T or x99 in (Cl T) \ T ) by A2, XBOOLE_0:def_3;
then A3: ( x99 in T or ( x99 in Cl T & x99 in T ` ) ) by XBOOLE_0:def_5;
 T ` c= Cl (T `) by PRE_TOPC:18;
then  ( x99 in T or x99 in (Cl T) /\ (Cl (T `)) ) by A3, XBOOLE_0:def_4;
hence  x in T \/ ((Cl T) /\ (Cl (T `))) by XBOOLE_0:def_3; ::_thesis: verum
end;
then A4: Cl T c= T \/ (Fr T) by PRE_TOPC:18, XBOOLE_1:45;
 T \/ (Fr T) = (T \/ (Cl T)) /\ (T \/ (Cl (T `))) by XBOOLE_1:24;
then  T \/ (Fr T) c= Cl T by A1, XBOOLE_1:17;
hence  Cl T = T \/ (Fr T) by A4, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th32: :: TOPS_1:32
for TS being TopSpace
for K, L being Subset of TS holds Fr (K /\ L) c= (Fr K) \/ (Fr L)
proof
let TS be TopSpace; ::_thesis: for K, L being Subset of TS holds Fr (K /\ L) c= (Fr K) \/ (Fr L)
let K, L be Subset of TS; ::_thesis: Fr (K /\ L) c= (Fr K) \/ (Fr L)
 Cl (K /\ L) c= Cl K by PRE_TOPC:19, XBOOLE_1:17;
then A1: (Cl (K /\ L)) /\ (Cl (K `)) c= (Cl K) /\ (Cl (K `)) by XBOOLE_1:26;
 Cl (K /\ L) c= Cl L by PRE_TOPC:19, XBOOLE_1:17;
then A2: (Cl (K /\ L)) /\ (Cl (L `)) c= (Cl L) /\ (Cl (L `)) by XBOOLE_1:26;
Fr (K /\ L) = (Cl (K /\ L)) /\ (Cl ((K `) \/ (L `))) by XBOOLE_1:54
.= (Cl (K /\ L)) /\ ((Cl (K `)) \/ (Cl (L `))) by PRE_TOPC:20
.= ((Cl (K /\ L)) /\ (Cl (K `))) \/ ((Cl (K /\ L)) /\ (Cl (L `))) by XBOOLE_1:23 ;
hence  Fr (K /\ L) c= (Fr K) \/ (Fr L) by A1, A2, XBOOLE_1:13; ::_thesis: verum
end;

theorem Th33: :: TOPS_1:33
for TS being TopSpace
for K, L being Subset of TS holds Fr (K \/ L) c= (Fr K) \/ (Fr L)
proof
let TS be TopSpace; ::_thesis: for K, L being Subset of TS holds Fr (K \/ L) c= (Fr K) \/ (Fr L)
let K, L be Subset of TS; ::_thesis: Fr (K \/ L) c= (Fr K) \/ (Fr L)
 Cl ((K `) /\ (L `)) c= Cl (K `) by PRE_TOPC:19, XBOOLE_1:17;
then A1: (Cl ((K `) /\ (L `))) /\ (Cl K) c= (Cl (K `)) /\ (Cl K) by XBOOLE_1:26;
 Cl ((K `) /\ (L `)) c= Cl (L `) by PRE_TOPC:19, XBOOLE_1:17;
then A2: (Cl ((K `) /\ (L `))) /\ (Cl L) c= (Cl (L `)) /\ (Cl L) by XBOOLE_1:26;
Fr (K \/ L) = ((Cl K) \/ (Cl L)) /\ (Cl ((K \/ L) `)) by PRE_TOPC:20
.= (Cl ((K `) /\ (L `))) /\ ((Cl K) \/ (Cl L)) by XBOOLE_1:53
.= ((Cl ((K `) /\ (L `))) /\ (Cl K)) \/ ((Cl ((K `) /\ (L `))) /\ (Cl L)) by XBOOLE_1:23 ;
hence  Fr (K \/ L) c= (Fr K) \/ (Fr L) by A1, A2, XBOOLE_1:13; ::_thesis: verum
end;

theorem Th34: :: TOPS_1:34
for GX being TopStruct
for T being Subset of GX holds Fr (Fr T) c= Fr T
proof
let GX be TopStruct ; ::_thesis: for T being Subset of GX holds Fr (Fr T) c= Fr T
let T be Subset of GX; ::_thesis: Fr (Fr T) c= Fr T
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Fr (Fr T) or x in Fr T )
assume  x in Fr (Fr T) ; ::_thesis: x in Fr T
then A1: x in Cl ((Cl T) /\ (Cl (T `))) by XBOOLE_0:def_4;
 Cl ((Cl T) /\ (Cl (T `))) c= (Cl (Cl T)) /\ (Cl (Cl (T `))) by PRE_TOPC:21;
hence  x in Fr T by A1; ::_thesis: verum
end;

theorem :: TOPS_1:35
for GX being TopStruct
for R being Subset of GX st R is closed holds
Fr R c= R
proof
let GX be TopStruct ; ::_thesis: for R being Subset of GX st R is closed holds
Fr R c= R
let R be Subset of GX; ::_thesis: ( R is closed implies Fr R c= R )
assume A1: R is closed ; ::_thesis: Fr R c= R
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Fr R or x in R )
 Cl R = R by A1, PRE_TOPC:22;
hence  ( not x in Fr R or x in R ) by XBOOLE_0:def_4; ::_thesis: verum
end;

Lm1:  for TS being TopSpace
for K, L being Subset of TS holds Fr K c= ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L))
proof
let TS be TopSpace; ::_thesis: for K, L being Subset of TS holds Fr K c= ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L))
let K, L be Subset of TS; ::_thesis: Fr K c= ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Fr K or x in ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) )
A1: (L `) /\ (K `) = (K \/ L) ` by XBOOLE_1:53;
assume A2: x in Fr K ; ::_thesis: x in ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L))
then reconsider x99 = x as Point of TS ;
A3: not TS is empty by A2;
assume A4: not x in ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) ; ::_thesis: contradiction
then A5: not x99 in (Fr (K \/ L)) \/ (Fr (K /\ L)) by XBOOLE_0:def_3;
then  not x99 in Fr (K \/ L) by XBOOLE_0:def_3;
then consider Q1 being Subset of TS such that
A6: Q1 is open and
A7: x99 in Q1 and
A8: ( K \/ L misses Q1 or (K \/ L) ` misses Q1 ) by A3, Th28;
 ( (K \/ L) /\ Q1 = {} or ((K \/ L) `) /\ Q1 = {} ) by A8, XBOOLE_0:def_7;
then A9: ( (K /\ Q1) \/ (Q1 /\ L) = {} or (L `) /\ ((K `) /\ Q1) = {} ) by A1, XBOOLE_1:16, XBOOLE_1:23;
 not x99 in (Fr K) /\ (Fr L) by A4, XBOOLE_0:def_3;
then  not x99 in Fr L by A2, XBOOLE_0:def_4;
then consider Q3 being Subset of TS such that
A10: Q3 is open and
A11: x99 in Q3 and
A12: ( L misses Q3 or L ` misses Q3 ) by A3, Th28;
 K meets Q1 by A2, A3, A6, A7, Th28;
then A13: K /\ Q1 <> {} by XBOOLE_0:def_7;
A14: now__::_thesis:_(_L_/\_Q3_=_{}_implies_(K_`)_/\_(Q1_/\_Q3)_=_{}_)
assume  L /\ Q3 = {} ; ::_thesis: (K `) /\ (Q1 /\ Q3) = {}
then  Q3 misses (L `) ` by XBOOLE_0:def_7;
then A15: Q3 c= L ` by SUBSET_1:24;
 ((K `) /\ Q1) /\ ((L `) /\ Q3) = {} /\ Q3 by A9, A13, XBOOLE_1:16;
then  ((K `) /\ Q1) /\ Q3 = {} by A15, XBOOLE_1:28;
hence  (K `) /\ (Q1 /\ Q3) = {} by XBOOLE_1:16; ::_thesis: verum
end;
A16: (L `) \/ (K `) = (K /\ L) ` by XBOOLE_1:54;
 not x99 in Fr (K /\ L) by A5, XBOOLE_0:def_3;
then consider Q2 being Subset of TS such that
A17: Q2 is open and
A18: x99 in Q2 and
A19: ( K /\ L misses Q2 or (K /\ L) ` misses Q2 ) by A3, Th28;
 ( (K /\ L) /\ Q2 = {} or ((K /\ L) `) /\ Q2 = {} ) by A19, XBOOLE_0:def_7;
then A20: ( (K /\ Q2) /\ L = {} or ((K `) /\ Q2) \/ (Q2 /\ (L `)) = {} ) by A16, XBOOLE_1:16, XBOOLE_1:23;
 x99 in Q1 /\ Q3 by A7, A11, XBOOLE_0:def_4;
then  K ` meets Q1 /\ Q3 by A2, A3, A6, A10, Th28;
then A21: Q3 c= L by A12, A14, SUBSET_1:24, XBOOLE_0:def_7;
 K ` meets Q2 by A2, A3, A17, A18, Th28;
then  (K `) /\ Q2 <> {} by XBOOLE_0:def_7;
then  (K /\ (Q2 /\ L)) /\ Q3 = {} /\ Q3 by A20, XBOOLE_1:16;
then  K /\ ((Q2 /\ L) /\ Q3) = {} by XBOOLE_1:16;
then  K /\ (Q2 /\ (L /\ Q3)) = {} by XBOOLE_1:16;
then  K /\ (Q2 /\ Q3) = {} by A21, XBOOLE_1:28;
then A22: K misses Q2 /\ Q3 by XBOOLE_0:def_7;
 x99 in Q2 /\ Q3 by A18, A11, XBOOLE_0:def_4;
hence  contradiction by A2, A3, A17, A10, A22, Th28; ::_thesis: verum
end;

theorem :: TOPS_1:36
for TS being TopSpace
for K, L being Subset of TS holds (Fr K) \/ (Fr L) = ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L))
proof
let TS be TopSpace; ::_thesis: for K, L being Subset of TS holds (Fr K) \/ (Fr L) = ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L))
let K, L be Subset of TS; ::_thesis: (Fr K) \/ (Fr L) = ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L))
A1: Fr L c= ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) by Lm1;
A2: ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) c= (Fr K) \/ (Fr L)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) or x in (Fr K) \/ (Fr L) )
A3: now__::_thesis:_(_x_in_(Fr_K)_/\_(Fr_L)_&_x_in_((Fr_(K_\/_L))_\/_(Fr_(K_/\_L)))_\/_((Fr_K)_/\_(Fr_L))_implies_x_in_(Fr_K)_\/_(Fr_L)_)
assume  x in (Fr K) /\ (Fr L) ; ::_thesis: ( not x in ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) or x in (Fr K) \/ (Fr L) )
then  x in Fr K by XBOOLE_0:def_4;
hence  ( not x in ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) or x in (Fr K) \/ (Fr L) ) by XBOOLE_0:def_3; ::_thesis: verum
end;
A4: now__::_thesis:_(_x_in_Fr_(K_\/_L)_&_x_in_((Fr_(K_\/_L))_\/_(Fr_(K_/\_L)))_\/_((Fr_K)_/\_(Fr_L))_implies_x_in_(Fr_K)_\/_(Fr_L)_)
assume A5: x in Fr (K \/ L) ; ::_thesis: ( not x in ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) or x in (Fr K) \/ (Fr L) )
 Fr (K \/ L) c= (Fr K) \/ (Fr L) by Th33;
hence  ( not x in ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) or x in (Fr K) \/ (Fr L) ) by A5; ::_thesis: verum
end;
A6: now__::_thesis:_(_x_in_Fr_(K_/\_L)_&_x_in_((Fr_(K_\/_L))_\/_(Fr_(K_/\_L)))_\/_((Fr_K)_/\_(Fr_L))_implies_x_in_(Fr_K)_\/_(Fr_L)_)
assume A7: x in Fr (K /\ L) ; ::_thesis: ( not x in ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) or x in (Fr K) \/ (Fr L) )
 Fr (K /\ L) c= (Fr K) \/ (Fr L) by Th32;
hence  ( not x in ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) or x in (Fr K) \/ (Fr L) ) by A7; ::_thesis: verum
end;
assume  x in ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) ; ::_thesis: x in (Fr K) \/ (Fr L)
then  ( x in (Fr (K \/ L)) \/ (Fr (K /\ L)) or x in (Fr K) /\ (Fr L) ) by XBOOLE_0:def_3;
hence  x in (Fr K) \/ (Fr L) by A4, A6, A3, XBOOLE_0:def_3; ::_thesis: verum
end;
 Fr K c= ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) by Lm1;
then  (Fr K) \/ (Fr L) c= ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) by A1, XBOOLE_1:8;
hence  (Fr K) \/ (Fr L) = ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L)) by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: TOPS_1:37
for GX being TopStruct
for T being Subset of GX holds Fr (Int T) c= Fr T
proof
let GX be TopStruct ; ::_thesis: for T being Subset of GX holds Fr (Int T) c= Fr T
let T be Subset of GX; ::_thesis: Fr (Int T) c= Fr T
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Fr (Int T) or x in Fr T )
assume A1: x in Fr (Int T) ; ::_thesis: x in Fr T
then A2: x in Cl (T `) by XBOOLE_0:def_4;
 Int T = (Cl (T `)) ` ;
then A3: Cl ((Cl (T `)) `) c= Cl T by Th16, PRE_TOPC:19;
 x in Cl ((Cl (T `)) `) by A1, XBOOLE_0:def_4;
hence  x in Fr T by A2, A3, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem :: TOPS_1:38
for GX being TopStruct
for T being Subset of GX holds Fr (Cl T) c= Fr T
proof
let GX be TopStruct ; ::_thesis: for T being Subset of GX holds Fr (Cl T) c= Fr T
let T be Subset of GX; ::_thesis: Fr (Cl T) c= Fr T
 T c= Cl T by PRE_TOPC:18;
then  (Cl T) ` c= T ` by SUBSET_1:12;
then  Cl ((Cl T) `) c= Cl (T `) by PRE_TOPC:19;
hence  Fr (Cl T) c= Fr T by XBOOLE_1:26; ::_thesis: verum
end;

theorem Th39: :: TOPS_1:39
for GX being TopStruct
for T being Subset of GX holds Int T misses Fr T
proof
let GX be TopStruct ; ::_thesis: for T being Subset of GX holds Int T misses Fr T
let T be Subset of GX; ::_thesis: Int T misses Fr T
Fr T = (Cl T) /\ (((Cl (T `)) `) `)
.= (Cl T) \ ((Cl (T `)) `) by SUBSET_1:13 ;
hence  Int T misses Fr T by XBOOLE_1:79; ::_thesis: verum
end;

theorem Th40: :: TOPS_1:40
for GX being TopStruct
for T being Subset of GX holds Int T = T \ (Fr T)
proof
let GX be TopStruct ; ::_thesis: for T being Subset of GX holds Int T = T \ (Fr T)
let T be Subset of GX; ::_thesis: Int T = T \ (Fr T)
 ((Cl (T `)) `) \/ ((Cl T) `) = ((Cl T) /\ (Cl (T `))) ` by XBOOLE_1:54;
then A1: T \ (Fr T) = T /\ (((Cl (T `)) `) \/ ((Cl T) `)) by SUBSET_1:13
.= (T /\ ((Cl T) `)) \/ (T /\ (Int T)) by XBOOLE_1:23 ;
 T c= Cl T by PRE_TOPC:18;
then A2: T misses (Cl T) ` by SUBSET_1:24;
 Int T = T /\ (Int T) by Th16, XBOOLE_1:28;
then  T \ (Fr T) = {} \/ (Int T) by A1, A2, XBOOLE_0:def_7;
hence  Int T = T \ (Fr T) ; ::_thesis: verum
end;

Lm2:  for GX being TopStruct
for T being Subset of GX holds Fr T = (Cl T) \ (Int T)
proof
let GX be TopStruct ; ::_thesis: for T being Subset of GX holds Fr T = (Cl T) \ (Int T)
let T be Subset of GX; ::_thesis: Fr T = (Cl T) \ (Int T)
Fr T = (Cl T) /\ ((Int T) `)
.= (Cl T) \ (Int T) by SUBSET_1:13 ;
hence  Fr T = (Cl T) \ (Int T) ; ::_thesis: verum
end;

Lm3:  for TS being TopSpace
for K being Subset of TS holds Cl (Fr K) = Fr K
proof
let TS be TopSpace; ::_thesis: for K being Subset of TS holds Cl (Fr K) = Fr K
let K be Subset of TS; ::_thesis: Cl (Fr K) = Fr K
A1: Cl (Cl (K `)) = Cl (K `) ;
 Cl (Cl K) = Cl K ;
hence  Cl (Fr K) = Fr K by A1, Th7; ::_thesis: verum
end;

Lm4:  for TS being TopSpace
for K being Subset of TS holds Int (Fr (Fr K)) = {}
proof
let TS be TopSpace; ::_thesis: for K being Subset of TS holds Int (Fr (Fr K)) = {}
let K be Subset of TS; ::_thesis: Int (Fr (Fr K)) = {}
set x9 = the Element of Int (Fr (Fr K));
assume A1: Int (Fr (Fr K)) <> {} ; ::_thesis: contradiction
then reconsider x = the Element of Int (Fr (Fr K)) as Point of TS by TARSKI:def_3;
A2: not TS is empty by A1;
A3: Int (Fr (Fr K)) c= Fr (Fr K) by Th16;
then  x in Fr (Fr K) by A1, TARSKI:def_3;
then  (Fr K) ` meets Int (Fr (Fr K)) by A1, A2, Th28;
then A4: ((Fr K) `) /\ (Int (Fr (Fr K))) <> {} by XBOOLE_0:def_7;
 Fr (Fr K) c= Fr K by Th34;
then  Int (Fr (Fr K)) c= Fr K by A3, XBOOLE_1:1;
then A5: ((Fr K) `) /\ (Fr K) <> {} by A4, XBOOLE_1:3, XBOOLE_1:26;
 Fr K misses (Fr K) ` by XBOOLE_1:79;
hence  contradiction by A5, XBOOLE_0:def_7; ::_thesis: verum
end;

theorem :: TOPS_1:41
for TS being TopSpace
for K being Subset of TS holds Fr (Fr (Fr K)) = Fr (Fr K)
proof
let TS be TopSpace; ::_thesis: for K being Subset of TS holds Fr (Fr (Fr K)) = Fr (Fr K)
let K be Subset of TS; ::_thesis: Fr (Fr (Fr K)) = Fr (Fr K)
A1: Int (Fr (Fr K)) = {} by Lm4;
Fr (Fr (Fr K)) = (Cl (Fr (Fr K))) \ (Int (Fr (Fr K))) by Lm2
.= Fr (Fr K) by A1, Lm3 ;
hence  Fr (Fr (Fr K)) = Fr (Fr K) ; ::_thesis: verum
end;

Lm5:  for X, Y, Z being set st X c= Z & Y = Z \ X holds
X c= Z \ Y
proof
let X, Y, Z be set ; ::_thesis: ( X c= Z & Y = Z \ X implies X c= Z \ Y )
assume that
A1: X c= Z and
A2: Y = Z \ X ; ::_thesis: X c= Z \ Y
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Z \ Y )
assume A3: x in X ; ::_thesis: x in Z \ Y
then  not x in Y by A2, XBOOLE_0:def_5;
hence  x in Z \ Y by A1, A3, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem Th42: :: TOPS_1:42
for TS being TopSpace
for P being Subset of TS holds
( P is open iff Fr P = (Cl P) \ P )
proof
let TS be TopSpace; ::_thesis: for P being Subset of TS holds
( P is open iff Fr P = (Cl P) \ P )
let P be Subset of TS; ::_thesis: ( P is open iff Fr P = (Cl P) \ P )
A1: Fr P misses (Fr P) ` by XBOOLE_1:79;
A2: Int P c= P by Th16;
hereby  ::_thesis: ( Fr P = (Cl P) \ P implies P is open )
assume  P is open ; ::_thesis: Fr P = (Cl P) \ P
then  P = Int P by Th23;
hence  Fr P = (Cl P) \ P by Lm2; ::_thesis: verum
end;
assume A3: Fr P = (Cl P) \ P ; ::_thesis: P is open
(Cl P) \ (Fr P) = (P \/ (Fr P)) \ (Fr P) by Th31
.= ((Fr P) `) /\ (P \/ (Fr P)) by SUBSET_1:13
.= (P /\ ((Fr P) `)) \/ (((Fr P) `) /\ (Fr P)) by XBOOLE_1:23
.= (P \ (Fr P)) \/ ((Fr P) /\ ((Fr P) `)) by SUBSET_1:13
.= (Int P) \/ ((Fr P) /\ ((Fr P) `)) by Th40
.= (Int P) \/ ({} TS) by A1, XBOOLE_0:def_7
.= Int P ;
then  P c= Int P by A3, Lm5, PRE_TOPC:18;
hence  P is open by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th43: :: TOPS_1:43
for TS being TopSpace
for P being Subset of TS holds
( P is closed iff Fr P = P \ (Int P) )
proof
let TS be TopSpace; ::_thesis: for P being Subset of TS holds
( P is closed iff Fr P = P \ (Int P) )
let P be Subset of TS; ::_thesis: ( P is closed iff Fr P = P \ (Int P) )
A1: P ` misses P by XBOOLE_1:79;
 (P `) /\ (Int P) c= (P `) /\ P by Th16, XBOOLE_1:26;
then A2: (P `) /\ (Int P) c= {} TS by A1, XBOOLE_0:def_7;
thus  ( P is closed implies Fr P = P \ (Int P) ) ::_thesis: ( Fr P = P \ (Int P) implies P is closed )
proof
assume  P is closed ; ::_thesis: Fr P = P \ (Int P)
then  P = Cl P by PRE_TOPC:22;
hence  Fr P = P \ (Int P) by Lm2; ::_thesis: verum
end;
A3: ((P `) `) \/ ((Int P) `) = ((P `) /\ (Int P)) ` by XBOOLE_1:54;
assume  Fr P = P \ (Int P) ; ::_thesis: P is closed
then  Cl P = P \/ (P \ (Int P)) by Th31
.= P \/ (((Int P) `) /\ P) by SUBSET_1:13
.= (P \/ ((Int P) `)) /\ (P \/ P) by XBOOLE_1:24
.= (({} TS) `) /\ P by A2, A3
.= P by XBOOLE_1:28 ;
hence  P is closed ; ::_thesis: verum
end;

definition
let GX be TopStruct ;
let R be Subset of GX;
attrR is dense  means :Def3: :: TOPS_1:def 3
 Cl R = [#] GX;
end;

:: deftheorem Def3 defines dense TOPS_1:def_3_:_
 for GX being TopStruct
for R being Subset of GX holds
( R is dense iff Cl R = [#] GX );

registration
let GX be TopStruct ;
cluster [#] GX ->  dense ;
coherence
 [#] GX is dense
proof
thus  Cl ([#] GX) = [#] GX by Th2; :: according to TOPS_1:def_3 ::_thesis: verum
end;
cluster dense for Element of K10( the carrier of GX);
existence
 ex b1 being Subset of GX st b1 is dense
proof
take  [#] GX ; ::_thesis: [#] GX is dense
thus  [#] GX is dense ; ::_thesis: verum
end;
end;

theorem :: TOPS_1:44
for GX being TopStruct
for R, S being Subset of GX st R is dense & R c= S holds
S is dense
proof
let GX be TopStruct ; ::_thesis: for R, S being Subset of GX st R is dense & R c= S holds
S is dense
let R, S be Subset of GX; ::_thesis: ( R is dense & R c= S implies S is dense )
assume that
A1: R is dense and
A2: R c= S ; ::_thesis: S is dense
 Cl R = [#] GX by A1, Def3;
then  [#] GX c= Cl S by A2, PRE_TOPC:19;
then  [#] GX = Cl S by XBOOLE_0:def_10;
hence  S is dense by Def3; ::_thesis: verum
end;

theorem Th45: :: TOPS_1:45
for TS being TopSpace
for P being Subset of TS holds
( P is dense iff for Q being Subset of TS st Q <> {} & Q is open holds
P meets Q )
proof
let TS be TopSpace; ::_thesis: for P being Subset of TS holds
( P is dense iff for Q being Subset of TS st Q <> {} & Q is open holds
P meets Q )
let P be Subset of TS; ::_thesis: ( P is dense iff for Q being Subset of TS st Q <> {} & Q is open holds
P meets Q )
hereby  ::_thesis: ( ( for Q being Subset of TS st Q <> {} & Q is open holds
P meets Q ) implies P is dense )
assume  P is dense ; ::_thesis: for Q being Subset of TS st Q <> {} & Q is open holds
P meets Q
then A1: Cl P = [#] TS by Def3;
let Q be Subset of TS; ::_thesis: ( Q <> {} & Q is open implies P meets Q )
assume that
A2: Q <> {} and
A3: Q is open ; ::_thesis: P meets Q
set x = the Element of Q;
 the Element of Q in Q by A2;
then A4: not TS is empty ;
 the Element of Q in Cl P by A2, A1, TARSKI:def_3;
hence  P meets Q by A2, A3, A4, Th12; ::_thesis: verum
end;
assume A5: for Q being Subset of TS st Q <> {} & Q is open holds
P meets Q ; ::_thesis: P is dense
 [#] TS c= Cl P
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [#] TS or x in Cl P )
A6: for C being Subset of TS st C is open & x in C holds
P meets C by A5;
assume A7: x in [#] TS ; ::_thesis: x in Cl P
then  not TS is empty ;
hence  x in Cl P by A7, A6, Th12; ::_thesis: verum
end;
then  Cl P = [#] TS by XBOOLE_0:def_10;
hence  P is dense by Def3; ::_thesis: verum
end;

theorem Th46: :: TOPS_1:46
for TS being TopSpace
for P being Subset of TS st P is dense holds
for Q being Subset of TS st Q is open holds
Cl Q = Cl (Q /\ P)
proof
let TS be TopSpace; ::_thesis: for P being Subset of TS st P is dense holds
for Q being Subset of TS st Q is open holds
Cl Q = Cl (Q /\ P)
let P be Subset of TS; ::_thesis: ( P is dense implies for Q being Subset of TS st Q is open holds
Cl Q = Cl (Q /\ P) )
assume A1: P is dense ; ::_thesis: for Q being Subset of TS st Q is open holds
Cl Q = Cl (Q /\ P)
let Q be Subset of TS; ::_thesis: ( Q is open implies Cl Q = Cl (Q /\ P) )
assume A2: Q is open ; ::_thesis: Cl Q = Cl (Q /\ P)
thus  Cl Q c= Cl (Q /\ P) :: according to XBOOLE_0:def_10 ::_thesis: Cl (Q /\ P) c= Cl Q
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl Q or x in Cl (Q /\ P) )
assume A3: x in Cl Q ; ::_thesis: x in Cl (Q /\ P)
then A4: not TS is empty ;
now__::_thesis:_for_Q1_being_Subset_of_TS_st_Q1_is_open_&_x_in_Q1_holds_
Q_/\_P_meets_Q1
let Q1 be Subset of TS; ::_thesis: ( Q1 is open & x in Q1 implies Q /\ P meets Q1 )
assume A5: Q1 is open ; ::_thesis: ( x in Q1 implies Q /\ P meets Q1 )
assume  x in Q1 ; ::_thesis: Q /\ P meets Q1
then  Q meets Q1 by A3, A4, A5, Th12;
then  Q /\ Q1 <> {} by XBOOLE_0:def_7;
then  P meets Q /\ Q1 by A1, A2, A5, Th45;
then A6: P /\ (Q /\ Q1) <> {} by XBOOLE_0:def_7;
 P /\ (Q /\ Q1) = (Q /\ P) /\ Q1 by XBOOLE_1:16;
hence  Q /\ P meets Q1 by A6, XBOOLE_0:def_7; ::_thesis: verum
end;
hence  x in Cl (Q /\ P) by A3, A4, Th12; ::_thesis: verum
end;
thus  Cl (Q /\ P) c= Cl Q by PRE_TOPC:19, XBOOLE_1:17; ::_thesis: verum
end;

theorem :: TOPS_1:47
for TS being TopSpace
for P, Q being Subset of TS st P is dense & Q is dense & Q is open holds
P /\ Q is dense
proof
let TS be TopSpace; ::_thesis: for P, Q being Subset of TS st P is dense & Q is dense & Q is open holds
P /\ Q is dense
let P, Q be Subset of TS; ::_thesis: ( P is dense & Q is dense & Q is open implies P /\ Q is dense )
assume that
A1: P is dense and
A2: Cl Q = [#] TS and
A3: Q is open ; :: according to TOPS_1:def_3 ::_thesis: P /\ Q is dense
thus  Cl (P /\ Q) = [#] TS by A1, A2, A3, Th46; :: according to TOPS_1:def_3 ::_thesis: verum
end;

definition
let GX be TopStruct ;
let R be Subset of GX;
attrR is boundary  means :Def4: :: TOPS_1:def 4
R ` is dense ;
end;

:: deftheorem Def4 defines boundary TOPS_1:def_4_:_
 for GX being TopStruct
for R being Subset of GX holds
( R is boundary iff R ` is dense );

registration
let GX be TopStruct ;
cluster empty  ->  boundary for Element of K10( the carrier of GX);
coherence
 for b1 being Subset of GX st b1 is empty holds
b1 is boundary
proof
let A be Subset of GX; ::_thesis: ( A is empty implies A is boundary )
assume  A is empty ; ::_thesis: A is boundary
hence  Cl (A `) = [#] GX by Th2; :: according to TOPS_1:def_3,TOPS_1:def_4 ::_thesis: verum
end;
end;

theorem Th48: :: TOPS_1:48
for GX being TopStruct
for R being Subset of GX holds
( R is boundary iff Int R = {} )
proof
let GX be TopStruct ; ::_thesis: for R being Subset of GX holds
( R is boundary iff Int R = {} )
let R be Subset of GX; ::_thesis: ( R is boundary iff Int R = {} )
 ( R is boundary iff R ` is dense ) by Def4;
then  ( R is boundary iff Cl (R `) = [#] GX ) by Def3;
then  ( R is boundary iff (Cl (R `)) ` = ([#] GX) ` ) by SUBSET_1:42;
hence  ( R is boundary iff Int R = {} ) by XBOOLE_1:37; ::_thesis: verum
end;

registration
let GX be TopStruct ;
cluster boundary for Element of K10( the carrier of GX);
existence
 ex b1 being Subset of GX st b1 is boundary
proof
take  {} GX ; ::_thesis: {} GX is boundary
thus  {} GX is boundary ; ::_thesis: verum
end;
end;

registration
let GX be TopStruct ;
let R be boundary Subset of GX;
cluster Int R ->  empty ;
coherence
 Int R is empty by Th48;
end;

theorem Th49: :: TOPS_1:49
for TS being TopSpace
for P, Q being Subset of TS st P is boundary & Q is boundary & Q is closed holds
P \/ Q is boundary
proof
let TS be TopSpace; ::_thesis: for P, Q being Subset of TS st P is boundary & Q is boundary & Q is closed holds
P \/ Q is boundary
let P, Q be Subset of TS; ::_thesis: ( P is boundary & Q is boundary & Q is closed implies P \/ Q is boundary )
assume that
A1: P is boundary and
A2: Q is boundary and
A3: Q is closed ; ::_thesis: P \/ Q is boundary
A4: Cl ((P `) \ Q) = Cl ((P `) /\ (Q `)) by SUBSET_1:13;
 P ` is dense by A1, Def4;
then A5: ([#] TS) \ Q = (Cl (P `)) \ Q by Def3;
A6: (Cl (P `)) \ (Cl Q) c= Cl ((P `) \ Q) by Th6;
 Q ` is dense by A2, Def4;
then A7: Cl (Q `) = [#] TS by Def3;
 (Cl (P `)) \ Q = (Cl (P `)) \ (Cl Q) by A3, PRE_TOPC:22;
then  ([#] TS) \ Q c= Cl ((P \/ Q) `) by A5, A6, A4, XBOOLE_1:53;
then  Cl (Q `) c= Cl (Cl ((P \/ Q) `)) by PRE_TOPC:19;
then  [#] TS = Cl ((P \/ Q) `) by A7, XBOOLE_0:def_10;
then  (P \/ Q) ` is dense by Def3;
hence  P \/ Q is boundary by Def4; ::_thesis: verum
end;

theorem :: TOPS_1:50
for TS being TopSpace
for P being Subset of TS holds
( P is boundary iff for Q being Subset of TS st Q c= P & Q is open holds
Q = {} )
proof
let TS be TopSpace; ::_thesis: for P being Subset of TS holds
( P is boundary iff for Q being Subset of TS st Q c= P & Q is open holds
Q = {} )
let P be Subset of TS; ::_thesis: ( P is boundary iff for Q being Subset of TS st Q c= P & Q is open holds
Q = {} )
hereby  ::_thesis: ( ( for Q being Subset of TS st Q c= P & Q is open holds
Q = {} ) implies P is boundary )
assume  P is boundary ; ::_thesis: for Q being Subset of TS st Q c= P & Q is open holds
not Q <> {}
then A1: P ` is dense by Def4;
let Q be Subset of TS; ::_thesis: ( Q c= P & Q is open implies not Q <> {} )
assume that
A2: Q c= P and
A3: Q is open and
A4: Q <> {} ; ::_thesis: contradiction
 Q meets P ` by A1, A3, A4, Th45;
hence  contradiction by A2, SUBSET_1:24; ::_thesis: verum
end;
assume A5: for Q being Subset of TS st Q c= P & Q is open holds
Q = {} ; ::_thesis: P is boundary
assume  not P is boundary ; ::_thesis: contradiction
then  not P ` is dense by Def4;
then consider C being Subset of TS such that
A6: C <> {} and
A7: C is open and
A8: P ` misses C by Th45;
 C c= P by A8, SUBSET_1:24;
hence  contradiction by A5, A6, A7; ::_thesis: verum
end;

theorem :: TOPS_1:51
for TS being TopSpace
for P being Subset of TS st P is closed holds
( P is boundary iff for Q being Subset of TS st Q <> {} & Q is open holds
ex G being Subset of TS st
( G c= Q & G <> {} & G is open & P misses G ) )
proof
let TS be TopSpace; ::_thesis: for P being Subset of TS st P is closed holds
( P is boundary iff for Q being Subset of TS st Q <> {} & Q is open holds
ex G being Subset of TS st
( G c= Q & G <> {} & G is open & P misses G ) )
let P be Subset of TS; ::_thesis: ( P is closed implies ( P is boundary iff for Q being Subset of TS st Q <> {} & Q is open holds
ex G being Subset of TS st
( G c= Q & G <> {} & G is open & P misses G ) ) )
assume A1: P is closed ; ::_thesis: ( P is boundary iff for Q being Subset of TS st Q <> {} & Q is open holds
ex G being Subset of TS st
( G c= Q & G <> {} & G is open & P misses G ) )
hereby  ::_thesis: ( ( for Q being Subset of TS st Q <> {} & Q is open holds
ex G being Subset of TS st
( G c= Q & G <> {} & G is open & P misses G ) ) implies P is boundary )
assume  P is boundary ; ::_thesis: for Q being Subset of TS st Q <> {} & Q is open holds
ex G being Subset of TS st
( G c= Q & G <> {} & G is open & P misses G )
then A2: P ` is dense by Def4;
A3: P misses P ` by XBOOLE_1:79;
let Q be Subset of TS; ::_thesis: ( Q <> {} & Q is open implies ex G being Subset of TS st
( G c= Q & G <> {} & G is open & P misses G ) )
assume that
A4: Q <> {} and
A5: Q is open ; ::_thesis: ex G being Subset of TS st
( G c= Q & G <> {} & G is open & P misses G )
P /\ ((P `) /\ Q) = (P /\ (P `)) /\ Q by XBOOLE_1:16
.= ({} TS) /\ Q by A3, XBOOLE_0:def_7
.= {} ;
then A6: P misses (P `) /\ Q by XBOOLE_0:def_7;
 P ` meets Q by A2, A4, A5, Th45;
then  (P `) /\ Q <> {} by XBOOLE_0:def_7;
hence  ex G being Subset of TS st
( G c= Q & G <> {} & G is open & P misses G ) by A1, A5, A6, XBOOLE_1:17; ::_thesis: verum
end;
assume A7: for Q being Subset of TS st Q <> {} & Q is open holds
ex G being Subset of TS st
( G c= Q & G <> {} & G is open & P misses G ) ; ::_thesis: P is boundary
now__::_thesis:_for_Q_being_Subset_of_TS_st_Q_<>_{}_&_Q_is_open_holds_
P_`_meets_Q
let Q be Subset of TS; ::_thesis: ( Q <> {} & Q is open implies P ` meets Q )
assume that
A8: Q <> {} and
A9: Q is open ; ::_thesis: P ` meets Q
consider G being Subset of TS such that
A10: G c= Q and
A11: G <> {} and
 G is open and
A12: P misses G by A7, A8, A9;
 G misses (P `) ` by A12;
then  G c= P ` by SUBSET_1:24;
hence  P ` meets Q by A10, A11, XBOOLE_1:67; ::_thesis: verum
end;
then  P ` is dense by Th45;
hence  P is boundary by Def4; ::_thesis: verum
end;

theorem :: TOPS_1:52
for GX being TopStruct
for R being Subset of GX holds
( R is boundary iff R c= Fr R )
proof
let GX be TopStruct ; ::_thesis: for R being Subset of GX holds
( R is boundary iff R c= Fr R )
let R be Subset of GX; ::_thesis: ( R is boundary iff R c= Fr R )
A1: (Cl R) /\ (Cl (R `)) c= Cl (R `) by XBOOLE_1:17;
hereby  ::_thesis: ( R c= Fr R implies R is boundary )
assume  R is boundary ; ::_thesis: R c= Fr R
then  R ` is dense by Def4;
then  (Cl R) /\ (Cl (R `)) = (Cl R) /\ ([#] GX) by Def3;
then  Cl R = (Cl R) /\ (Cl (R `)) by XBOOLE_1:28;
hence  R c= Fr R by PRE_TOPC:18; ::_thesis: verum
end;
A2: R ` c= Cl (R `) by PRE_TOPC:18;
assume  R c= Fr R ; ::_thesis: R is boundary
then  R c= Cl (R `) by A1, XBOOLE_1:1;
then  R \/ (R `) c= Cl (R `) by A2, XBOOLE_1:8;
then  [#] GX c= Cl (R `) by PRE_TOPC:2;
then  [#] GX = Cl (R `) by XBOOLE_0:def_10;
then  R ` is dense by Def3;
hence  R is boundary by Def4; ::_thesis: verum
end;

registration
let GX be non empty TopSpace;
cluster [#] GX ->  non boundary ;
coherence
 not [#] GX is boundary
proof
 Int ([#] GX) <> {} by Th15;
hence  not [#] GX is boundary ; ::_thesis: verum
end;
cluster non empty non boundary for Element of K10( the carrier of GX);
existence
 ex b1 being Subset of GX st
( not b1 is boundary & not b1 is empty )
proof
take  [#] GX ; ::_thesis: ( not [#] GX is boundary & not [#] GX is empty )
thus  ( not [#] GX is boundary & not [#] GX is empty ) ; ::_thesis: verum
end;
end;

definition
let GX be TopStruct ;
let R be Subset of GX;
attrR is nowhere_dense  means :Def5: :: TOPS_1:def 5
 Cl R is boundary ;
end;

:: deftheorem Def5 defines nowhere_dense TOPS_1:def_5_:_
 for GX being TopStruct
for R being Subset of GX holds
( R is nowhere_dense iff Cl R is boundary );

registration
let TS be TopSpace;
cluster empty  ->  nowhere_dense for Element of K10( the carrier of TS);
coherence
 for b1 being Subset of TS st b1 is empty holds
b1 is nowhere_dense
proof
let A be Subset of TS; ::_thesis: ( A is empty implies A is nowhere_dense )
A1: (Cl ({} TS)) ` = ({} TS) ` by PRE_TOPC:22
.= [#] TS ;
assume  A is empty ; ::_thesis: A is nowhere_dense
hence  (Cl A) ` is dense by A1; :: according to TOPS_1:def_4,TOPS_1:def_5 ::_thesis: verum
end;
end;

registration
let TS be TopSpace;
cluster nowhere_dense for Element of K10( the carrier of TS);
existence
 ex b1 being Subset of TS st b1 is nowhere_dense
proof
take  {} TS ; ::_thesis: {} TS is nowhere_dense
thus  {} TS is nowhere_dense ; ::_thesis: verum
end;
end;

theorem :: TOPS_1:53
for TS being TopSpace
for P, Q being Subset of TS st P is nowhere_dense & Q is nowhere_dense holds
P \/ Q is nowhere_dense
proof
let TS be TopSpace; ::_thesis: for P, Q being Subset of TS st P is nowhere_dense & Q is nowhere_dense holds
P \/ Q is nowhere_dense
let P, Q be Subset of TS; ::_thesis: ( P is nowhere_dense & Q is nowhere_dense implies P \/ Q is nowhere_dense )
assume that
A1: P is nowhere_dense and
A2: Q is nowhere_dense ; ::_thesis: P \/ Q is nowhere_dense
A3: Cl Q is boundary by A2, Def5;
 Cl P is boundary by A1, Def5;
then  (Cl P) \/ (Cl Q) is boundary by A3, Th49;
then  Cl (P \/ Q) is boundary by PRE_TOPC:20;
hence  P \/ Q is nowhere_dense by Def5; ::_thesis: verum
end;

theorem Th54: :: TOPS_1:54
for GX being TopStruct
for R being Subset of GX st R is nowhere_dense holds
R ` is dense
proof
let GX be TopStruct ; ::_thesis: for R being Subset of GX st R is nowhere_dense holds
R ` is dense
let R be Subset of GX; ::_thesis: ( R is nowhere_dense implies R ` is dense )
assume  R is nowhere_dense ; ::_thesis: R ` is dense
then  Cl R is boundary by Def5;
then  (Cl R) ` is dense by Def4;
then A1: Cl ((Cl R) `) = [#] GX by Def3;
 R c= Cl R by PRE_TOPC:18;
then  (Cl R) ` c= R ` by SUBSET_1:12;
then  [#] GX c= Cl (R `) by A1, PRE_TOPC:19;
then  [#] GX = Cl (R `) by XBOOLE_0:def_10;
hence  R ` is dense by Def3; ::_thesis: verum
end;

registration
let TS be TopSpace;
let R be nowhere_dense Subset of TS;
clusterR `  ->  dense ;
coherence
 R ` is dense by Th54;
end;

theorem Th55: :: TOPS_1:55
for GX being TopStruct
for R being Subset of GX st R is nowhere_dense holds
R is boundary
proof
let GX be TopStruct ; ::_thesis: for R being Subset of GX st R is nowhere_dense holds
R is boundary
let R be Subset of GX; ::_thesis: ( R is nowhere_dense implies R is boundary )
assume  R is nowhere_dense ; ::_thesis: R is boundary
then  R ` is dense by Th54;
hence  R is boundary by Def4; ::_thesis: verum
end;

registration
let TS be TopSpace;
cluster nowhere_dense  ->  boundary for Element of K10( the carrier of TS);
coherence
 for b1 being Subset of TS st b1 is nowhere_dense holds
b1 is boundary by Th55;
end;

theorem Th56: :: TOPS_1:56
for GX being TopStruct
for S being Subset of GX st S is boundary & S is closed holds
S is nowhere_dense
proof
let GX be TopStruct ; ::_thesis: for S being Subset of GX st S is boundary & S is closed holds
S is nowhere_dense
let S be Subset of GX; ::_thesis: ( S is boundary & S is closed implies S is nowhere_dense )
assume that
A1: S is boundary and
A2: S is closed ; ::_thesis: S is nowhere_dense
 Cl S is boundary by A1, A2, PRE_TOPC:22;
hence  S is nowhere_dense by Def5; ::_thesis: verum
end;

registration
let TS be TopSpace;
cluster closed boundary  ->  nowhere_dense for Element of K10( the carrier of TS);
coherence
 for b1 being Subset of TS st b1 is boundary & b1 is closed holds
b1 is nowhere_dense by Th56;
end;

theorem :: TOPS_1:57
for GX being TopStruct
for R being Subset of GX st R is closed holds
( R is nowhere_dense iff R = Fr R )
proof
let GX be TopStruct ; ::_thesis: for R being Subset of GX st R is closed holds
( R is nowhere_dense iff R = Fr R )
let R be Subset of GX; ::_thesis: ( R is closed implies ( R is nowhere_dense iff R = Fr R ) )
assume  R is closed ; ::_thesis: ( R is nowhere_dense iff R = Fr R )
then A1: R = Cl R by PRE_TOPC:22;
hereby  ::_thesis: ( R = Fr R implies R is nowhere_dense )
assume  R is nowhere_dense ; ::_thesis: R = Fr R
then  Cl R is boundary by Def5;
then  (Cl R) ` is dense by Def4;
then  Fr R = R /\ ([#] GX) by A1, Def3;
hence  R = Fr R by XBOOLE_1:28; ::_thesis: verum
end;
assume  R = Fr R ; ::_thesis: R is nowhere_dense
then  R = R \ (Int R) by A1, Lm2;
then  Int (Cl R) = {} by A1, Th16, XBOOLE_1:38;
then  Cl R is boundary by Th48;
hence  R is nowhere_dense by Def5; ::_thesis: verum
end;

theorem Th58: :: TOPS_1:58
for TS being TopSpace
for P being Subset of TS st P is open holds
Fr P is nowhere_dense
proof
let TS be TopSpace; ::_thesis: for P being Subset of TS st P is open holds
Fr P is nowhere_dense
let P be Subset of TS; ::_thesis: ( P is open implies Fr P is nowhere_dense )
A1: Int (Cl P) c= Cl P by Th16;
assume  P is open ; ::_thesis: Fr P is nowhere_dense
then A2: Int P = P by Th23;
then  P misses Fr P by Th39;
then A3: P /\ (Fr P) = {} TS by XBOOLE_0:def_7;
 Int (P /\ (Fr P)) = P /\ (Int (Fr P)) by A2, Th17;
then  P /\ (Int (Fr P)) = {} by A3;
then A4: P misses Int (Fr P) by XBOOLE_0:def_7;
 Int (Fr P) c= Int (Cl P) by Th19, XBOOLE_1:17;
then A5: Int (Fr P) c= Cl P by A1, XBOOLE_1:1;
 Fr P is boundary
proof
set x = the Element of Int (Fr P);
assume A6: not Fr P is boundary ; ::_thesis: contradiction
then A7: not TS is empty ;
A8: Int (Fr P) <> {} by A6, Th48;
then  the Element of Int (Fr P) in Cl P by A5, TARSKI:def_3;
hence  contradiction by A4, A8, A7, Th12; ::_thesis: verum
end;
hence  Fr P is nowhere_dense ; ::_thesis: verum
end;

registration
let TS be TopSpace;
let P be open Subset of TS;
cluster Fr P ->  nowhere_dense ;
coherence
 Fr P is nowhere_dense by Th58;
end;

theorem Th59: :: TOPS_1:59
for TS being TopSpace
for P being Subset of TS st P is closed holds
Fr P is nowhere_dense
proof
let TS be TopSpace; ::_thesis: for P being Subset of TS st P is closed holds
Fr P is nowhere_dense
let P be Subset of TS; ::_thesis: ( P is closed implies Fr P is nowhere_dense )
assume  P is closed ; ::_thesis: Fr P is nowhere_dense
then  Fr (P `) is nowhere_dense ;
hence  Fr P is nowhere_dense ; ::_thesis: verum
end;

registration
let TS be TopSpace;
let P be closed Subset of TS;
cluster Fr P ->  nowhere_dense ;
coherence
 Fr P is nowhere_dense by Th59;
end;

theorem Th60: :: TOPS_1:60
for TS being TopSpace
for P being Subset of TS st P is open & P is nowhere_dense holds
P = {}
proof
let TS be TopSpace; ::_thesis: for P being Subset of TS st P is open & P is nowhere_dense holds
P = {}
let P be Subset of TS; ::_thesis: ( P is open & P is nowhere_dense implies P = {} )
assume that
A1: P is open and
A2: P is nowhere_dense and
A3: P <> {} ; ::_thesis: contradiction
 P meets P ` by A1, A2, A3, Th45;
hence  contradiction by XBOOLE_1:79; ::_thesis: verum
end;

registration
let TS be TopSpace;
cluster open nowhere_dense  ->  empty for Element of K10( the carrier of TS);
coherence
 for b1 being Subset of TS st b1 is open & b1 is nowhere_dense holds
b1 is empty by Th60;
end;

definition
let GX be TopStruct ;
let R be Subset of GX;
attrR is condensed  means :Def6: :: TOPS_1:def 6
( Int (Cl R) c= R & R c= Cl (Int R) );
attrR is closed_condensed  means :Def7: :: TOPS_1:def 7
R = Cl (Int R);
attrR is open_condensed  means :Def8: :: TOPS_1:def 8
R = Int (Cl R);
end;

:: deftheorem Def6 defines condensed TOPS_1:def_6_:_
 for GX being TopStruct
for R being Subset of GX holds
( R is condensed iff ( Int (Cl R) c= R & R c= Cl (Int R) ) );

:: deftheorem Def7 defines closed_condensed TOPS_1:def_7_:_
 for GX being TopStruct
for R being Subset of GX holds
( R is closed_condensed iff R = Cl (Int R) );

:: deftheorem Def8 defines open_condensed TOPS_1:def_8_:_
 for GX being TopStruct
for R being Subset of GX holds
( R is open_condensed iff R = Int (Cl R) );

theorem Th61: :: TOPS_1:61
for GX being TopStruct
for R being Subset of GX holds
( R is open_condensed iff R ` is closed_condensed )
proof
let GX be TopStruct ; ::_thesis: for R being Subset of GX holds
( R is open_condensed iff R ` is closed_condensed )
let R be Subset of GX; ::_thesis: ( R is open_condensed iff R ` is closed_condensed )
 ( R is open_condensed iff R = Int (Cl R) ) by Def8;
then  ( R is open_condensed iff R ` = Cl (Int (R `)) ) ;
hence  ( R is open_condensed iff R ` is closed_condensed ) by Def7; ::_thesis: verum
end;

theorem Th62: :: TOPS_1:62
for GX being TopStruct
for R being Subset of GX st R is closed_condensed holds
Fr (Int R) = Fr R
proof
let GX be TopStruct ; ::_thesis: for R being Subset of GX st R is closed_condensed holds
Fr (Int R) = Fr R
let R be Subset of GX; ::_thesis: ( R is closed_condensed implies Fr (Int R) = Fr R )
assume  R is closed_condensed ; ::_thesis: Fr (Int R) = Fr R
then  R = Cl (Int R) by Def7;
hence  Fr (Int R) = Fr R ; ::_thesis: verum
end;

theorem :: TOPS_1:63
for GX being TopStruct
for R being Subset of GX st R is closed_condensed holds
Fr R c= Cl (Int R)
proof
let GX be TopStruct ; ::_thesis: for R being Subset of GX st R is closed_condensed holds
Fr R c= Cl (Int R)
let R be Subset of GX; ::_thesis: ( R is closed_condensed implies Fr R c= Cl (Int R) )
assume  R is closed_condensed ; ::_thesis: Fr R c= Cl (Int R)
then  R = Cl (Int R) by Def7;
hence  Fr R c= Cl (Int R) by XBOOLE_1:17; ::_thesis: verum
end;

theorem Th64: :: TOPS_1:64
for GX being TopStruct
for R being Subset of GX st R is open_condensed holds
( Fr R = Fr (Cl R) & Fr (Cl R) = (Cl R) \ R )
proof
let GX be TopStruct ; ::_thesis: for R being Subset of GX st R is open_condensed holds
( Fr R = Fr (Cl R) & Fr (Cl R) = (Cl R) \ R )
let R be Subset of GX; ::_thesis: ( R is open_condensed implies ( Fr R = Fr (Cl R) & Fr (Cl R) = (Cl R) \ R ) )
assume  R is open_condensed ; ::_thesis: ( Fr R = Fr (Cl R) & Fr (Cl R) = (Cl R) \ R )
then  R = Int (Cl R) by Def8;
hence  ( Fr R = Fr (Cl R) & Fr (Cl R) = (Cl R) \ R ) by Lm2; ::_thesis: verum
end;

theorem :: TOPS_1:65
for GX being TopStruct
for R being Subset of GX st R is open & R is closed holds
( R is closed_condensed iff R is open_condensed )
proof
let GX be TopStruct ; ::_thesis: for R being Subset of GX st R is open & R is closed holds
( R is closed_condensed iff R is open_condensed )
let R be Subset of GX; ::_thesis: ( R is open & R is closed implies ( R is closed_condensed iff R is open_condensed ) )
assume that
A1: R is open and
A2: R is closed ; ::_thesis: ( R is closed_condensed iff R is open_condensed )
A3: R = Cl R by A2, PRE_TOPC:22;
 R = Int R by A1, Th23;
hence  ( R is closed_condensed iff R is open_condensed ) by A3, Def7, Def8; ::_thesis: verum
end;

theorem Th66: :: TOPS_1:66
for TS being TopSpace
for GX being TopStruct
for P being Subset of TS
for R being Subset of GX holds
( ( R is closed & R is condensed implies R is closed_condensed ) & ( P is closed_condensed implies ( P is closed & P is condensed ) ) )
proof
let TS be TopSpace; ::_thesis: for GX being TopStruct
for P being Subset of TS
for R being Subset of GX holds
( ( R is closed & R is condensed implies R is closed_condensed ) & ( P is closed_condensed implies ( P is closed & P is condensed ) ) )
let GX be TopStruct ; ::_thesis: for P being Subset of TS
for R being Subset of GX holds
( ( R is closed & R is condensed implies R is closed_condensed ) & ( P is closed_condensed implies ( P is closed & P is condensed ) ) )
let P be Subset of TS; ::_thesis: for R being Subset of GX holds
( ( R is closed & R is condensed implies R is closed_condensed ) & ( P is closed_condensed implies ( P is closed & P is condensed ) ) )
let R be Subset of GX; ::_thesis: ( ( R is closed & R is condensed implies R is closed_condensed ) & ( P is closed_condensed implies ( P is closed & P is condensed ) ) )
hereby  ::_thesis: ( P is closed_condensed implies ( P is closed & P is condensed ) )
assume that
A1: R is closed and
A2: R is condensed ; ::_thesis: R is closed_condensed
A3: R = Cl R by A1, PRE_TOPC:22;
then  Int R c= R by A2, Def6;
then A4: Cl (Int R) c= R by A3, PRE_TOPC:19;
 R c= Cl (Int R) by A2, Def6;
then  Cl (Int R) = R by A4, XBOOLE_0:def_10;
hence  R is closed_condensed by Def7; ::_thesis: verum
end;
assume A5: P is closed_condensed ; ::_thesis: ( P is closed & P is condensed )
 Fr (Int P) = (Cl (Int P)) \ (Int (Int P)) by Lm2;
then  Fr P = (Cl (Int P)) \ (Int (Int P)) by A5, Th62
.= P \ (Int P) by A5, Def7 ;
then  P is closed by Th43;
then  Cl P = P by PRE_TOPC:22;
then A6: Int (Cl P) c= P by Th16;
 Cl (Int P) = P by A5, Def7;
hence  ( P is closed & P is condensed ) by A6, Def6; ::_thesis: verum
end;

theorem :: TOPS_1:67
for TS being TopSpace
for GX being TopStruct
for P being Subset of TS
for R being Subset of GX holds
( ( R is open & R is condensed implies R is open_condensed ) & ( P is open_condensed implies ( P is open & P is condensed ) ) )
proof
let TS be TopSpace; ::_thesis: for GX being TopStruct
for P being Subset of TS
for R being Subset of GX holds
( ( R is open & R is condensed implies R is open_condensed ) & ( P is open_condensed implies ( P is open & P is condensed ) ) )
let GX be TopStruct ; ::_thesis: for P being Subset of TS
for R being Subset of GX holds
( ( R is open & R is condensed implies R is open_condensed ) & ( P is open_condensed implies ( P is open & P is condensed ) ) )
let P be Subset of TS; ::_thesis: for R being Subset of GX holds
( ( R is open & R is condensed implies R is open_condensed ) & ( P is open_condensed implies ( P is open & P is condensed ) ) )
let R be Subset of GX; ::_thesis: ( ( R is open & R is condensed implies R is open_condensed ) & ( P is open_condensed implies ( P is open & P is condensed ) ) )
hereby  ::_thesis: ( P is open_condensed implies ( P is open & P is condensed ) )
assume that
A1: R is open and
A2: R is condensed ; ::_thesis: R is open_condensed
 R = Int R by A1, Th23;
then A3: R c= Int (Cl R) by Th19, PRE_TOPC:18;
 Int (Cl R) c= R by A2, Def6;
then  Int (Cl R) = R by A3, XBOOLE_0:def_10;
hence  R is open_condensed by Def8; ::_thesis: verum
end;
assume A4: P is open_condensed ; ::_thesis: ( P is open & P is condensed )
then A5: Fr (Cl P) = (Cl P) \ P by Th64;
 Fr P = Fr (Cl P) by A4, Th64;
then  P is open by A5, Th42;
then  Int P = P by Th23;
then A6: P c= Cl (Int P) by PRE_TOPC:18;
 P = Int (Cl P) by A4, Def8;
hence  ( P is open & P is condensed ) by A6, Def6; ::_thesis: verum
end;

theorem Th68: :: TOPS_1:68
for TS being TopSpace
for P, Q being Subset of TS st P is closed_condensed & Q is closed_condensed holds
P \/ Q is closed_condensed
proof
let TS be TopSpace; ::_thesis: for P, Q being Subset of TS st P is closed_condensed & Q is closed_condensed holds
P \/ Q is closed_condensed
let P, Q be Subset of TS; ::_thesis: ( P is closed_condensed & Q is closed_condensed implies P \/ Q is closed_condensed )
assume that
A1: P is closed_condensed and
A2: Q is closed_condensed ; ::_thesis: P \/ Q is closed_condensed
A3: Q = Cl (Int Q) by A2, Def7;
 P = Cl (Int P) by A1, Def7;
then  P \/ Q = Cl ((Int P) \/ (Int Q)) by A3, PRE_TOPC:20;
then A4: P \/ Q c= Cl (Int (P \/ Q)) by Th20, PRE_TOPC:19;
A5: Cl (Int (P \/ Q)) c= Cl (P \/ Q) by Th16, PRE_TOPC:19;
A6: Q is closed by A2, Th66;
 P is closed by A1, Th66;
then  Cl (Int (P \/ Q)) c= P \/ Q by A5, A6, PRE_TOPC:22;
then  P \/ Q = Cl (Int (P \/ Q)) by A4, XBOOLE_0:def_10;
hence  P \/ Q is closed_condensed by Def7; ::_thesis: verum
end;

theorem :: TOPS_1:69
for TS being TopSpace
for P, Q being Subset of TS st P is open_condensed & Q is open_condensed holds
P /\ Q is open_condensed
proof
let TS be TopSpace; ::_thesis: for P, Q being Subset of TS st P is open_condensed & Q is open_condensed holds
P /\ Q is open_condensed
let P, Q be Subset of TS; ::_thesis: ( P is open_condensed & Q is open_condensed implies P /\ Q is open_condensed )
A1: (P `) \/ (Q `) = (P /\ Q) ` by XBOOLE_1:54;
assume that
A2: P is open_condensed and
A3: Q is open_condensed ; ::_thesis: P /\ Q is open_condensed
A4: Q ` is closed_condensed by A3, Th61;
 P ` is closed_condensed by A2, Th61;
then  (P `) \/ (Q `) is closed_condensed by A4, Th68;
hence  P /\ Q is open_condensed by A1, Th61; ::_thesis: verum
end;

theorem :: TOPS_1:70
for TS being TopSpace
for P being Subset of TS st P is condensed holds
Int (Fr P) = {}
proof
let TS be TopSpace; ::_thesis: for P being Subset of TS st P is condensed holds
Int (Fr P) = {}
let P be Subset of TS; ::_thesis: ( P is condensed implies Int (Fr P) = {} )
set x = the Element of Int (Fr P);
assume A1: P is condensed ; ::_thesis: Int (Fr P) = {}
then  P c= Cl (Int P) by Def6;
then A2: (Cl (Int P)) ` c= P ` by SUBSET_1:12;
assume A3: Int (Fr P) <> {} ; ::_thesis: contradiction
then reconsider x99 = the Element of Int (Fr P) as Point of TS by TARSKI:def_3;
A4: Int (Fr P) = (Cl (((Cl P) `) \/ ((Cl (P `)) `))) ` by XBOOLE_1:54
.= ((Cl ((Cl P) `)) \/ (Cl ((Cl (P `)) `))) ` by PRE_TOPC:20
.= (Int (Cl P)) /\ ((Cl (Int P)) `) by XBOOLE_1:53 ;
then A5: x99 in Int (Cl P) by A3, XBOOLE_0:def_4;
A6: x99 in (Cl (Int P)) ` by A4, A3, XBOOLE_0:def_4;
 Int (Cl P) c= P by A1, Def6;
hence  contradiction by A2, A5, A6, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem :: TOPS_1:71
for GX being TopStruct
for R being Subset of GX st R is condensed holds
( Int R is condensed & Cl R is condensed )
proof
let GX be TopStruct ; ::_thesis: for R being Subset of GX st R is condensed holds
( Int R is condensed & Cl R is condensed )
let R be Subset of GX; ::_thesis: ( R is condensed implies ( Int R is condensed & Cl R is condensed ) )
 Cl (Int R) c= Cl R by Th16, PRE_TOPC:19;
then A1: Int (Cl (Int R)) c= Int (Cl R) by Th19;
A2: R c= Cl R by PRE_TOPC:18;
then  (Cl R) ` c= R ` by SUBSET_1:12;
then  Cl ((Cl R) `) c= Cl (R `) by PRE_TOPC:19;
then  (Cl (R `)) ` c= (Cl ((Cl R) `)) ` by SUBSET_1:12;
then A3: Cl (Int R) c= Cl ((Cl ((Cl R) `)) `) by PRE_TOPC:19;
assume A4: R is condensed ; ::_thesis: ( Int R is condensed & Cl R is condensed )
then A5: R c= Cl (Int R) by Def6;
then  Cl R c= Cl (Cl (Int R)) by PRE_TOPC:19;
then A6: Cl R c= Cl (Int (Cl R)) by A3, XBOOLE_1:1;
A7: Int (Cl R) c= R by A4, Def6;
then  Int (Int (Cl R)) c= Int R by Th19;
then A8: Int (Cl (Int R)) c= Int R by A1, XBOOLE_1:1;
 Int R c= R by Th16;
then A9: Int R c= Cl (Int (Int R)) by A5, XBOOLE_1:1;
 Int (Cl (Cl R)) c= Cl R by A7, A2, XBOOLE_1:1;
hence  ( Int R is condensed & Cl R is condensed ) by A9, A6, A8, Def6; ::_thesis: verum
end;