:: PRE_TOPC semantic presentation

begin

definition
attrc1 is strict ;
struct TopStruct  ->  1-sorted ;
aggrTopStruct(# carrier, topology #) ->  TopStruct ;
sel topology c1 ->  Subset-Family of the carrier of c1;
end;

definition
let IT be TopStruct ;
attrIT is TopSpace-like  means :Def1: :: PRE_TOPC:def 1
( the carrier of IT in the topology of IT & ( for a being Subset-Family of IT st a c= the topology of IT holds
union a in the topology of IT ) & ( for a, b being Subset of IT st a in the topology of IT & b in the topology of IT holds
a /\ b in the topology of IT ) );
end;

:: deftheorem Def1 defines TopSpace-like PRE_TOPC:def_1_:_
 for IT being TopStruct holds
( IT is TopSpace-like iff ( the carrier of IT in the topology of IT & ( for a being Subset-Family of IT st a c= the topology of IT holds
union a in the topology of IT ) & ( for a, b being Subset of IT st a in the topology of IT & b in the topology of IT holds
a /\ b in the topology of IT ) ) );

registration
cluster non empty strict TopSpace-like for TopStruct ;
existence
 ex b1 being TopStruct st
( not b1 is empty & b1 is strict & b1 is TopSpace-like )
proof
now__::_thesis:_ex_X_being_set_ex_T_being_Subset-Family_of_X_st_
(_the_carrier_of_TopStruct(#_X,T_#)_in_the_topology_of_TopStruct(#_X,T_#)_&_(_for_a_being_Subset-Family_of_TopStruct(#_X,T_#)_st_a_c=_the_topology_of_TopStruct(#_X,T_#)_holds_
union_a_in_the_topology_of_TopStruct(#_X,T_#)_)_&_(_for_a,_b_being_Subset_of_TopStruct(#_X,T_#)_st_a_in_the_topology_of_TopStruct(#_X,T_#)_&_b_in_the_topology_of_TopStruct(#_X,T_#)_holds_
a_/\_b_in_the_topology_of_TopStruct(#_X,T_#)_)_)
take X = {{}}; ::_thesis: ex T being Subset-Family of X st
( the carrier of TopStruct(# X,T #) in the topology of TopStruct(# X,T #) & ( for a being Subset-Family of TopStruct(# X,T #) st a c= the topology of TopStruct(# X,T #) holds
union a in the topology of TopStruct(# X,T #) ) & ( for a, b being Subset of TopStruct(# X,T #) st a in the topology of TopStruct(# X,T #) & b in the topology of TopStruct(# X,T #) holds
a /\ b in the topology of TopStruct(# X,T #) ) )
set T = {{},X};
 {{},X} c= bool X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{},X} or x in bool X )
assume  x in {{},X} ; ::_thesis: x in bool X
then  ( x = {} or x = X ) by TARSKI:def_2;
then  x c= X by XBOOLE_1:2;
hence  x in bool X ; ::_thesis: verum
end;
then reconsider T = {{},X} as Subset-Family of X ;
take T = T; ::_thesis: ( the carrier of TopStruct(# X,T #) in the topology of TopStruct(# X,T #) & ( for a being Subset-Family of TopStruct(# X,T #) st a c= the topology of TopStruct(# X,T #) holds
union a in the topology of TopStruct(# X,T #) ) & ( for a, b being Subset of TopStruct(# X,T #) st a in the topology of TopStruct(# X,T #) & b in the topology of TopStruct(# X,T #) holds
a /\ b in the topology of TopStruct(# X,T #) ) )
set Y = TopStruct(# X,T #);
thus  the carrier of TopStruct(# X,T #) in the topology of TopStruct(# X,T #) by TARSKI:def_2; ::_thesis: ( ( for a being Subset-Family of TopStruct(# X,T #) st a c= the topology of TopStruct(# X,T #) holds
union a in the topology of TopStruct(# X,T #) ) & ( for a, b being Subset of TopStruct(# X,T #) st a in the topology of TopStruct(# X,T #) & b in the topology of TopStruct(# X,T #) holds
a /\ b in the topology of TopStruct(# X,T #) ) )
thus  for a being Subset-Family of TopStruct(# X,T #) st a c= the topology of TopStruct(# X,T #) holds
union a in the topology of TopStruct(# X,T #) ::_thesis: for a, b being Subset of TopStruct(# X,T #) st a in the topology of TopStruct(# X,T #) & b in the topology of TopStruct(# X,T #) holds
a /\ b in the topology of TopStruct(# X,T #)
proof
let a be Subset-Family of TopStruct(# X,T #); ::_thesis: ( a c= the topology of TopStruct(# X,T #) implies union a in the topology of TopStruct(# X,T #) )
assume  a c= the topology of TopStruct(# X,T #) ; ::_thesis: union a in the topology of TopStruct(# X,T #)
then  ( a = {} or a = {{}} or a = {X} or a = {{},X} ) by ZFMISC_1:36;
then  ( union a = {} or union a = X or union a = {} \/ X ) by ZFMISC_1:2, ZFMISC_1:25, ZFMISC_1:75;
hence  union a in the topology of TopStruct(# X,T #) by TARSKI:def_2; ::_thesis: verum
end;
let a, b be Subset of TopStruct(# X,T #); ::_thesis: ( a in the topology of TopStruct(# X,T #) & b in the topology of TopStruct(# X,T #) implies a /\ b in the topology of TopStruct(# X,T #) )
assume that
A1: a in the topology of TopStruct(# X,T #) and
A2: b in the topology of TopStruct(# X,T #) ; ::_thesis: a /\ b in the topology of TopStruct(# X,T #)
A3: ( b = {} or b = X ) by A2, TARSKI:def_2;
 ( a = {} or a = X ) by A1, TARSKI:def_2;
hence  a /\ b in the topology of TopStruct(# X,T #) by A3, TARSKI:def_2; ::_thesis: verum
end;
then consider X being non empty set , T being Subset-Family of X such that
A4: ( the carrier of TopStruct(# X,T #) in the topology of TopStruct(# X,T #) & ( for a being Subset-Family of TopStruct(# X,T #) st a c= the topology of TopStruct(# X,T #) holds
union a in the topology of TopStruct(# X,T #) ) & ( for a, b being Subset of TopStruct(# X,T #) st a in the topology of TopStruct(# X,T #) & b in the topology of TopStruct(# X,T #) holds
a /\ b in the topology of TopStruct(# X,T #) ) ) ;
take  TopStruct(# X,T #) ; ::_thesis: ( not TopStruct(# X,T #) is empty & TopStruct(# X,T #) is strict & TopStruct(# X,T #) is TopSpace-like )
thus  not TopStruct(# X,T #) is empty ; ::_thesis: ( TopStruct(# X,T #) is strict & TopStruct(# X,T #) is TopSpace-like )
thus  ( TopStruct(# X,T #) is strict & TopStruct(# X,T #) is TopSpace-like ) by A4, Def1; ::_thesis: verum
end;
end;

definition
mode TopSpace is TopSpace-like TopStruct ;
end;

definition
let S be 1-sorted ;
mode Point of S is Element of S;
end;

registration
let T be TopSpace;
cluster the topology of T ->  non empty ;
coherence
 not the topology of T is empty by Def1;
end;

theorem Th1: :: PRE_TOPC:1
for GX being TopSpace holds {} in the topology of GX
proof
let GX be TopSpace; ::_thesis: {} in the topology of GX
reconsider A = {} as Subset-Family of GX by XBOOLE_1:2;
 A c= the topology of GX by XBOOLE_1:2;
hence  {} in the topology of GX by Def1, ZFMISC_1:2; ::_thesis: verum
end;

theorem :: PRE_TOPC:2
for T being 1-sorted
for P being Subset of T holds P \/ (P `) = [#] T
proof
let T be 1-sorted ; ::_thesis: for P being Subset of T holds P \/ (P `) = [#] T
let P be Subset of T; ::_thesis: P \/ (P `) = [#] T
P \/ (P `) = [#] the carrier of T by SUBSET_1:10
.= the carrier of T ;
hence  P \/ (P `) = [#] T ; ::_thesis: verum
end;

theorem Th3: :: PRE_TOPC:3
for T being 1-sorted
for P being Subset of T holds ([#] T) \ (([#] T) \ P) = P
proof
let T be 1-sorted ; ::_thesis: for P being Subset of T holds ([#] T) \ (([#] T) \ P) = P
let P be Subset of T; ::_thesis: ([#] T) \ (([#] T) \ P) = P
 ([#] T) \ (([#] T) \ P) = P /\ ([#] T) by XBOOLE_1:48;
hence  ([#] T) \ (([#] T) \ P) = P by XBOOLE_1:28; ::_thesis: verum
end;

theorem Th4: :: PRE_TOPC:4
for T being 1-sorted
for P being Subset of T holds
( P <> [#] T iff ([#] T) \ P <> {} )
proof
let T be 1-sorted ; ::_thesis: for P being Subset of T holds
( P <> [#] T iff ([#] T) \ P <> {} )
let P be Subset of T; ::_thesis: ( P <> [#] T iff ([#] T) \ P <> {} )
now__::_thesis:_(_P_<>_[#]_T_implies_not_([#]_T)_\_P_=_{}_)
assume that
A1: P <> [#] T and
A2: ([#] T) \ P = {} ; ::_thesis: contradiction
 [#] T c= P by A2, XBOOLE_1:37;
hence  contradiction by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
hence  ( P <> [#] T iff ([#] T) \ P <> {} ) by XBOOLE_1:37; ::_thesis: verum
end;

theorem :: PRE_TOPC:5
for T being 1-sorted
for P, Q being Subset of T st [#] T = P \/ Q & P misses Q holds
Q = ([#] T) \ P
proof
let T be 1-sorted ; ::_thesis: for P, Q being Subset of T st [#] T = P \/ Q & P misses Q holds
Q = ([#] T) \ P
let P, Q be Subset of T; ::_thesis: ( [#] T = P \/ Q & P misses Q implies Q = ([#] T) \ P )
assume that
A1: [#] T = P \/ Q and
A2: P misses Q ; ::_thesis: Q = ([#] T) \ P
([#] T) \ P = Q \ P by A1, XBOOLE_1:40
.= Q by A2, XBOOLE_1:83 ;
hence  Q = ([#] T) \ P ; ::_thesis: verum
end;

theorem :: PRE_TOPC:6
for T being 1-sorted holds [#] T = ({} T) ` ;

definition
let T be TopStruct ;
let P be Subset of T;
attrP is open  means :Def2: :: PRE_TOPC:def 2
P in the topology of T;
end;

:: deftheorem Def2 defines open PRE_TOPC:def_2_:_
 for T being TopStruct
for P being Subset of T holds
( P is open iff P in the topology of T );

definition
let T be TopStruct ;
let P be Subset of T;
attrP is closed  means :Def3: :: PRE_TOPC:def 3
([#] T) \ P is open ;
end;

:: deftheorem Def3 defines closed PRE_TOPC:def_3_:_
 for T being TopStruct
for P being Subset of T holds
( P is closed iff ([#] T) \ P is open );

definition
let T be TopStruct ;
mode SubSpace of T ->  TopStruct  means :Def4: :: PRE_TOPC:def 4
( [#] it c= [#] T & ( for P being Subset of it holds
( P in the topology of it iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] it) ) ) ) );
existence
 ex b1 being TopStruct st
( [#] b1 c= [#] T & ( for P being Subset of b1 holds
( P in the topology of b1 iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] b1) ) ) ) )
proof
take  T ; ::_thesis: ( [#] T c= [#] T & ( for P being Subset of T holds
( P in the topology of T iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] T) ) ) ) )
thus  [#] T c= [#] T ; ::_thesis: for P being Subset of T holds
( P in the topology of T iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] T) ) )
let P be Subset of T; ::_thesis: ( P in the topology of T iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] T) ) )
hereby  ::_thesis: ( ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] T) ) implies P in the topology of T )
assume A1: P in the topology of T ; ::_thesis: ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] T) )
take Q = P; ::_thesis: ( Q in the topology of T & P = Q /\ ([#] T) )
thus  Q in the topology of T by A1; ::_thesis: P = Q /\ ([#] T)
thus  P = Q /\ ([#] T) by XBOOLE_1:28; ::_thesis: verum
end;
given Q being Subset of T such that A2: ( Q in the topology of T & P = Q /\ ([#] T) ) ; ::_thesis: P in the topology of T
thus  P in the topology of T by A2, XBOOLE_1:28; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines SubSpace PRE_TOPC:def_4_:_
 for T, b2 being TopStruct holds
( b2 is SubSpace of T iff ( [#] b2 c= [#] T & ( for P being Subset of b2 holds
( P in the topology of b2 iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] b2) ) ) ) ) );

Lm1:  for T being TopStruct holds TopStruct(# the carrier of T, the topology of T #) is SubSpace of T
proof
let T be TopStruct ; ::_thesis: TopStruct(# the carrier of T, the topology of T #) is SubSpace of T
set S = TopStruct(# the carrier of T, the topology of T #);
thus  [#] TopStruct(# the carrier of T, the topology of T #) c= [#] T ; :: according to PRE_TOPC:def_4 ::_thesis: for P being Subset of TopStruct(# the carrier of T, the topology of T #) holds
( P in the topology of TopStruct(# the carrier of T, the topology of T #) iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) )
let P be Subset of TopStruct(# the carrier of T, the topology of T #); ::_thesis: ( P in the topology of TopStruct(# the carrier of T, the topology of T #) iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) )
hereby  ::_thesis: ( ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) implies P in the topology of TopStruct(# the carrier of T, the topology of T #) )
reconsider Q = P as Subset of T ;
assume A1: P in the topology of TopStruct(# the carrier of T, the topology of T #) ; ::_thesis: ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #)) )
take Q = Q; ::_thesis: ( Q in the topology of T & P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #)) )
thus  Q in the topology of T by A1; ::_thesis: P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #))
thus  P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #)) by XBOOLE_1:28; ::_thesis: verum
end;
given Q being Subset of T such that A2: ( Q in the topology of T & P = Q /\ ([#] TopStruct(# the carrier of T, the topology of T #)) ) ; ::_thesis: P in the topology of TopStruct(# the carrier of T, the topology of T #)
thus  P in the topology of TopStruct(# the carrier of T, the topology of T #) by A2, XBOOLE_1:28; ::_thesis: verum
end;

registration
let T be TopStruct ;
cluster strict for SubSpace of T;
existence
 ex b1 being SubSpace of T st b1 is strict
proof
 TopStruct(# the carrier of T, the topology of T #) is SubSpace of T by Lm1;
hence  ex b1 being SubSpace of T st b1 is strict ; ::_thesis: verum
end;
end;

registration
let T be non empty TopStruct ;
cluster non empty strict for SubSpace of T;
existence
 ex b1 being SubSpace of T st
( b1 is strict & not b1 is empty )
proof
 ( TopStruct(# the carrier of T, the topology of T #) is SubSpace of T & not TopStruct(# the carrier of T, the topology of T #) is empty ) by Lm1;
hence  ex b1 being SubSpace of T st
( b1 is strict & not b1 is empty ) ; ::_thesis: verum
end;
end;

registration
let T be TopSpace;
cluster  ->  TopSpace-like for SubSpace of T;
coherence
 for b1 being SubSpace of T holds b1 is TopSpace-like
proof
let S be SubSpace of T; ::_thesis: S is TopSpace-like
 S is TopSpace-like
proof
set P = the carrier of S;
A1: [#] T in the topology of T by Def1;
A2: the carrier of S = [#] S ;
then  the carrier of S c= [#] T by Def4;
then  ([#] T) /\ the carrier of S = the carrier of S by XBOOLE_1:28;
hence  the carrier of S in the topology of S by A2, A1, Def4; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for a being Subset-Family of S st a c= the topology of S holds
union a in the topology of S ) & ( for a, b being Subset of S st a in the topology of S & b in the topology of S holds
a /\ b in the topology of S ) )
thus  for a being Subset-Family of S st a c= the topology of S holds
union a in the topology of S ::_thesis: for a, b being Subset of S st a in the topology of S & b in the topology of S holds
a /\ b in the topology of S
proof
let a be Subset-Family of S; ::_thesis: ( a c= the topology of S implies union a in the topology of S )
assume A3: a c= the topology of S ; ::_thesis: union a in the topology of S
defpred S1[ set ] means ( T /\ the carrier of S in a & T in the topology of T );
consider b being Subset-Family of T such that
A4: for Z being Subset of T holds
( Z in b iff S1[Z] ) from SUBSET_1:sch_3();
A5: (union b) /\ the carrier of S c= union a
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (union b) /\ the carrier of S or x in union a )
assume A6: x in (union b) /\ the carrier of S ; ::_thesis: x in union a
then  x in union b by XBOOLE_0:def_4;
then consider Z being set  such that
A7: x in Z and
A8: Z in b by TARSKI:def_4;
 x in the carrier of S by A6, XBOOLE_0:def_4;
then A9: x in Z /\ the carrier of S by A7, XBOOLE_0:def_4;
 Z /\ the carrier of S in a by A4, A8;
hence  x in union a by A9, TARSKI:def_4; ::_thesis: verum
end;
 b c= the topology of T
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in b or y in the topology of T )
assume  y in b ; ::_thesis: y in the topology of T
hence  y in the topology of T by A4; ::_thesis: verum
end;
then A10: union b in the topology of T by Def1;
 union a c= (union b) /\ the carrier of S
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union a or x in (union b) /\ the carrier of S )
assume A11: x in union a ; ::_thesis: x in (union b) /\ the carrier of S
then consider Z1 being set  such that
A12: x in Z1 and
A13: Z1 in a by TARSKI:def_4;
consider Z3 being Subset of T such that
A14: ( Z3 in the topology of T & Z1 = Z3 /\ the carrier of S ) by A2, A3, A13, Def4;
 ( Z3 in b & x in Z3 ) by A4, A12, A13, A14, XBOOLE_0:def_4;
then  x in union b by TARSKI:def_4;
hence  x in (union b) /\ the carrier of S by A11, XBOOLE_0:def_4; ::_thesis: verum
end;
then  union a = (union b) /\ the carrier of S by A5, XBOOLE_0:def_10;
hence  union a in the topology of S by A2, A10, Def4; ::_thesis: verum
end;
thus  for V, Q being Subset of S st V in the topology of S & Q in the topology of S holds
V /\ Q in the topology of S ::_thesis: verum
proof
let V, Q be Subset of S; ::_thesis: ( V in the topology of S & Q in the topology of S implies V /\ Q in the topology of S )
assume that
A15: V in the topology of S and
A16: Q in the topology of S ; ::_thesis: V /\ Q in the topology of S
consider P1 being Subset of T such that
A17: P1 in the topology of T and
A18: V = P1 /\ the carrier of S by A2, A15, Def4;
consider Q1 being Subset of T such that
A19: Q1 in the topology of T and
A20: Q = Q1 /\ the carrier of S by A2, A16, Def4;
A21: V /\ Q = P1 /\ ((Q1 /\ the carrier of S) /\ the carrier of S) by A18, A20, XBOOLE_1:16
.= P1 /\ (Q1 /\ ( the carrier of S /\ the carrier of S)) by XBOOLE_1:16
.= (P1 /\ Q1) /\ the carrier of S by XBOOLE_1:16 ;
 P1 /\ Q1 in the topology of T by A17, A19, Def1;
hence  V /\ Q in the topology of S by A2, A21, Def4; ::_thesis: verum
end;
end;
hence  S is TopSpace-like ; ::_thesis: verum
end;
end;

definition
let T be TopStruct ;
let P be Subset of T;
funcT | P ->  strict SubSpace of T means :Def5: :: PRE_TOPC:def 5
 [#] it = P;
existence
 ex b1 being strict SubSpace of T st [#] b1 = P
proof
defpred S1[ set ] means  ex Q being Subset of T st
( Q in the topology of T & $1 = Q /\ P );
consider top1 being Subset-Family of P such that
A1: for Z being Subset of P holds
( Z in top1 iff S1[Z] ) from SUBSET_1:sch_3();
reconsider top1 = top1 as Subset-Family of P ;
set Y = TopStruct(# P,top1 #);
A2: for Z being Subset of TopStruct(# P,top1 #) holds
( Z in top1 iff ex Q being Subset of T st
( Q in the topology of T & Z = Q /\ ([#] TopStruct(# P,top1 #)) ) )
proof
let Z be Subset of TopStruct(# P,top1 #); ::_thesis: ( Z in top1 iff ex Q being Subset of T st
( Q in the topology of T & Z = Q /\ ([#] TopStruct(# P,top1 #)) ) )
thus  ( Z in top1 implies ex Q being Subset of T st
( Q in the topology of T & Z = Q /\ ([#] TopStruct(# P,top1 #)) ) ) ::_thesis: ( ex Q being Subset of T st
( Q in the topology of T & Z = Q /\ ([#] TopStruct(# P,top1 #)) ) implies Z in top1 )
proof
assume  Z in top1 ; ::_thesis: ex Q being Subset of T st
( Q in the topology of T & Z = Q /\ ([#] TopStruct(# P,top1 #)) )
then  S1[Z] by A1;
hence  ex Q being Subset of T st
( Q in the topology of T & Z = Q /\ ([#] TopStruct(# P,top1 #)) ) ; ::_thesis: verum
end;
thus  ( ex Q being Subset of T st
( Q in the topology of T & Z = Q /\ ([#] TopStruct(# P,top1 #)) ) implies Z in top1 ) by A1; ::_thesis: verum
end;
 [#] TopStruct(# P,top1 #) c= [#] T ;
then reconsider Y = TopStruct(# P,top1 #) as strict SubSpace of T by A2, Def4;
take  Y ; ::_thesis: [#] Y = P
thus  [#] Y = P ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict SubSpace of T st [#] b1 = P & [#] b2 = P holds
b1 = b2
proof
let Z1, Z2 be strict SubSpace of T; ::_thesis: ( [#] Z1 = P & [#] Z2 = P implies Z1 = Z2 )
assume A3: ( [#] Z1 = P & [#] Z2 = P ) ; ::_thesis: Z1 = Z2
A4: the topology of Z2 c= the topology of Z1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of Z2 or x in the topology of Z1 )
assume  x in the topology of Z2 ; ::_thesis: x in the topology of Z1
then  ex Q being Subset of T st
( Q in the topology of T & x = Q /\ ([#] Z1) ) by A3, Def4;
hence  x in the topology of Z1 by Def4; ::_thesis: verum
end;
 the topology of Z1 c= the topology of Z2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the topology of Z1 or x in the topology of Z2 )
assume  x in the topology of Z1 ; ::_thesis: x in the topology of Z2
then  ex Q being Subset of T st
( Q in the topology of T & x = Q /\ ([#] Z2) ) by A3, Def4;
hence  x in the topology of Z2 by Def4; ::_thesis: verum
end;
hence  Z1 = Z2 by A3, A4, XBOOLE_0:def_10; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines | PRE_TOPC:def_5_:_
 for T being TopStruct
for P being Subset of T
for b3 being strict SubSpace of T holds
( b3 = T | P iff [#] b3 = P );

registration
let T be non empty TopStruct ;
let P be non empty Subset of T;
clusterT | P ->  non empty strict ;
coherence
 not T | P is empty
proof
 [#] (T | P) = P by Def5;
hence  not the carrier of (T | P) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

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

registration
let T be TopSpace;
let P be Subset of T;
clusterT | P ->  strict TopSpace-like ;
coherence
 T | P is TopSpace-like ;
end;

theorem :: PRE_TOPC:7
for S being TopSpace
for P1, P2 being Subset of S
for P19 being Subset of (S | P2) st P1 = P19 & P1 c= P2 holds
S | P1 = (S | P2) | P19
proof
let S be TopSpace; ::_thesis: for P1, P2 being Subset of S
for P19 being Subset of (S | P2) st P1 = P19 & P1 c= P2 holds
S | P1 = (S | P2) | P19
let P1, P2 be Subset of S; ::_thesis: for P19 being Subset of (S | P2) st P1 = P19 & P1 c= P2 holds
S | P1 = (S | P2) | P19
let P19 be Subset of (S | P2); ::_thesis: ( P1 = P19 & P1 c= P2 implies S | P1 = (S | P2) | P19 )
assume that
A1: P1 = P19 and
A2: P1 c= P2 ; ::_thesis: S | P1 = (S | P2) | P19
A3: [#] ((S | P2) | P19) = P1 by A1, Def5;
A4: [#] (S | P2) = P2 by Def5;
A5: for R being Subset of ((S | P2) | P19) holds
( R in the topology of ((S | P2) | P19) iff ex Q being Subset of S st
( Q in the topology of S & R = Q /\ ([#] ((S | P2) | P19)) ) )
proof
let R be Subset of ((S | P2) | P19); ::_thesis: ( R in the topology of ((S | P2) | P19) iff ex Q being Subset of S st
( Q in the topology of S & R = Q /\ ([#] ((S | P2) | P19)) ) )
A6: now__::_thesis:_(_ex_Q_being_Subset_of_S_st_
(_Q_in_the_topology_of_S_&_R_=_Q_/\_([#]_((S_|_P2)_|_P19))_)_implies_R_in_the_topology_of_((S_|_P2)_|_P19)_)
given Q being Subset of S such that A7: Q in the topology of S and
A8: R = Q /\ ([#] ((S | P2) | P19)) ; ::_thesis: R in the topology of ((S | P2) | P19)
reconsider R9 = Q /\ ([#] (S | P2)) as Subset of (S | P2) ;
A9: R9 in the topology of (S | P2) by A7, Def4;
R9 /\ ([#] ((S | P2) | P19)) = Q /\ (P2 /\ P1) by A4, A3, XBOOLE_1:16
.= R by A2, A3, A8, XBOOLE_1:28 ;
hence  R in the topology of ((S | P2) | P19) by A9, Def4; ::_thesis: verum
end;
now__::_thesis:_(_R_in_the_topology_of_((S_|_P2)_|_P19)_implies_ex_Q_being_Subset_of_S_st_
(_Q_in_the_topology_of_S_&_R_=_Q_/\_([#]_((S_|_P2)_|_P19))_)_)
assume  R in the topology of ((S | P2) | P19) ; ::_thesis: ex Q being Subset of S st
( Q in the topology of S & R = Q /\ ([#] ((S | P2) | P19)) )
then consider Q0 being Subset of (S | P2) such that
A10: Q0 in the topology of (S | P2) and
A11: R = Q0 /\ ([#] ((S | P2) | P19)) by Def4;
consider Q1 being Subset of S such that
A12: Q1 in the topology of S and
A13: Q0 = Q1 /\ ([#] (S | P2)) by A10, Def4;
R = Q1 /\ (P2 /\ P1) by A4, A3, A11, A13, XBOOLE_1:16
.= Q1 /\ ([#] ((S | P2) | P19)) by A2, A3, XBOOLE_1:28 ;
hence  ex Q being Subset of S st
( Q in the topology of S & R = Q /\ ([#] ((S | P2) | P19)) ) by A12; ::_thesis: verum
end;
hence  ( R in the topology of ((S | P2) | P19) iff ex Q being Subset of S st
( Q in the topology of S & R = Q /\ ([#] ((S | P2) | P19)) ) ) by A6; ::_thesis: verum
end;
 [#] ((S | P2) | P19) c= [#] S by A3;
then  (S | P2) | P19 is SubSpace of S by A5, Def4;
hence  S | P1 = (S | P2) | P19 by A3, Def5; ::_thesis: verum
end;

theorem Th8: :: PRE_TOPC:8
for GX being TopStruct
for A being Subset of GX holds the carrier of (GX | A) = A
proof
let GX be TopStruct ; ::_thesis: for A being Subset of GX holds the carrier of (GX | A) = A
let A be Subset of GX; ::_thesis: the carrier of (GX | A) = A
 A = [#] (GX | A) by Def5;
hence  the carrier of (GX | A) = A ; ::_thesis: verum
end;

theorem :: PRE_TOPC:9
for X being TopStruct
for Y being non empty TopStruct
for f being Function of X,Y
for P being Subset of X holds f | P is Function of (X | P),Y
proof
let X be TopStruct ; ::_thesis: for Y being non empty TopStruct
for f being Function of X,Y
for P being Subset of X holds f | P is Function of (X | P),Y
let Y be non empty TopStruct ; ::_thesis: for f being Function of X,Y
for P being Subset of X holds f | P is Function of (X | P),Y
let f be Function of X,Y; ::_thesis: for P being Subset of X holds f | P is Function of (X | P),Y
let P be Subset of X; ::_thesis: f | P is Function of (X | P),Y
 P = the carrier of (X | P) by Th8;
hence  f | P is Function of (X | P),Y by FUNCT_2:32; ::_thesis: verum
end;

definition
let S, T be TopStruct ;
let f be Function of S,T;
attrf is continuous  means :Def6: :: PRE_TOPC:def 6
 for P1 being Subset of T st P1 is closed holds
f " P1 is closed ;
end;

:: deftheorem Def6 defines continuous PRE_TOPC:def_6_:_
 for S, T being TopStruct
for f being Function of S,T holds
( f is continuous iff for P1 being Subset of T st P1 is closed holds
f " P1 is closed );

theorem :: PRE_TOPC:10
for T1, T2, S1, S2 being TopStruct st TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) & TopStruct(# the carrier of S1, the topology of S1 #) = TopStruct(# the carrier of S2, the topology of S2 #) & S1 is SubSpace of T1 holds
S2 is SubSpace of T2
proof
let T1, T2, S1, S2 be TopStruct ; ::_thesis: ( TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) & TopStruct(# the carrier of S1, the topology of S1 #) = TopStruct(# the carrier of S2, the topology of S2 #) & S1 is SubSpace of T1 implies S2 is SubSpace of T2 )
assume A1: ( TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) & TopStruct(# the carrier of S1, the topology of S1 #) = TopStruct(# the carrier of S2, the topology of S2 #) ) ; ::_thesis: ( not S1 is SubSpace of T1 or S2 is SubSpace of T2 )
assume that
A2: [#] S1 c= [#] T1 and
A3: for P being Subset of S1 holds
( P in the topology of S1 iff ex Q being Subset of T1 st
( Q in the topology of T1 & P = Q /\ ([#] S1) ) ) ; :: according to PRE_TOPC:def_4 ::_thesis: S2 is SubSpace of T2
thus  [#] S2 c= [#] T2 by A1, A2; :: according to PRE_TOPC:def_4 ::_thesis: for P being Subset of S2 holds
( P in the topology of S2 iff ex Q being Subset of T2 st
( Q in the topology of T2 & P = Q /\ ([#] S2) ) )
thus  for P being Subset of S2 holds
( P in the topology of S2 iff ex Q being Subset of T2 st
( Q in the topology of T2 & P = Q /\ ([#] S2) ) ) by A1, A3; ::_thesis: verum
end;

theorem Th11: :: PRE_TOPC:11
for T being TopStruct
for X9 being SubSpace of T
for A being Subset of X9 holds A is Subset of T
proof
let T be TopStruct ; ::_thesis: for X9 being SubSpace of T
for A being Subset of X9 holds A is Subset of T
let X9 be SubSpace of T; ::_thesis: for A being Subset of X9 holds A is Subset of T
let A be Subset of X9; ::_thesis: A is Subset of T
 [#] X9 c= [#] T by Def4;
hence  A is Subset of T by XBOOLE_1:1; ::_thesis: verum
end;

theorem :: PRE_TOPC:12
for T being TopStruct
for A being Subset of T st A <> {} T holds
ex x being Point of T st x in A
proof
let T be TopStruct ; ::_thesis: for A being Subset of T st A <> {} T holds
ex x being Point of T st x in A
let A be Subset of T; ::_thesis: ( A <> {} T implies ex x being Point of T st x in A )
set x = the Element of A;
assume A1: A <> {} T ; ::_thesis: ex x being Point of T st x in A
then  the Element of A is Point of T by TARSKI:def_3;
hence  ex x being Point of T st x in A by A1; ::_thesis: verum
end;

registration
let T be TopSpace;
cluster [#] T ->  closed ;
coherence
 [#] T is closed
proof
 {} T in the topology of T by Th1;
then A1: {} T is open by Def2;
 ([#] T) \ ([#] T) = {} T by Th4;
hence  [#] T is closed by A1, Def3; ::_thesis: verum
end;
end;

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

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

theorem Th13: :: PRE_TOPC:13
for T being TopStruct
for X9 being SubSpace of T
for B being Subset of X9 holds
( B is closed iff ex C being Subset of T st
( C is closed & C /\ ([#] X9) = B ) )
proof
let T be TopStruct ; ::_thesis: for X9 being SubSpace of T
for B being Subset of X9 holds
( B is closed iff ex C being Subset of T st
( C is closed & C /\ ([#] X9) = B ) )
let X9 be SubSpace of T; ::_thesis: for B being Subset of X9 holds
( B is closed iff ex C being Subset of T st
( C is closed & C /\ ([#] X9) = B ) )
let B be Subset of X9; ::_thesis: ( B is closed iff ex C being Subset of T st
( C is closed & C /\ ([#] X9) = B ) )
A1: [#] X9 is Subset of T by Th11;
A2: now__::_thesis:_(_B_is_closed_implies_ex_C_being_Subset_of_T_st_
(_C_is_closed_&_C_/\_([#]_X9)_=_B_)_)
assume  B is closed ; ::_thesis: ex C being Subset of T st
( C is closed & C /\ ([#] X9) = B )
then  ([#] X9) \ B is open by Def3;
then  ([#] X9) \ B in the topology of X9 by Def2;
then consider V being Subset of T such that
A3: V in the topology of T and
A4: ([#] X9) \ B = V /\ ([#] X9) by Def4;
A5: (([#] T) \ V) /\ ([#] X9) = ([#] X9) /\ (V `)
.= ([#] X9) \ V by A1, SUBSET_1:13
.= ([#] X9) \ (([#] X9) /\ V) by XBOOLE_1:47
.= B by A4, Th3 ;
reconsider V1 = V as Subset of T ;
A6: ([#] T) \ (([#] T) \ V) = V by Th3;
 V1 is open by A3, Def2;
then  ([#] T) \ V is closed by A6, Def3;
hence  ex C being Subset of T st
( C is closed & C /\ ([#] X9) = B ) by A5; ::_thesis: verum
end;
now__::_thesis:_(_ex_C_being_Subset_of_T_st_
(_C_is_closed_&_C_/\_([#]_X9)_=_B_)_implies_B_is_closed_)
given C being Subset of T such that A7: C is closed and
A8: C /\ ([#] X9) = B ; ::_thesis: B is closed
 ([#] T) \ C is open by A7, Def3;
then  ([#] T) \ C in the topology of T by Def2;
then A9: (([#] T) \ C) /\ ([#] X9) in the topology of X9 by Def4;
([#] X9) \ B = ([#] X9) \ C by A8, XBOOLE_1:47
.= ([#] X9) /\ (C `) by A1, SUBSET_1:13
.= (([#] T) \ C) /\ ([#] X9) ;
then  ([#] X9) \ B is open by A9, Def2;
hence  B is closed by Def3; ::_thesis: verum
end;
hence  ( B is closed iff ex C being Subset of T st
( C is closed & C /\ ([#] X9) = B ) ) by A2; ::_thesis: verum
end;

theorem Th14: :: PRE_TOPC:14
for GX being TopSpace
for F being Subset-Family of GX st ( for A being Subset of GX st A in F holds
A is closed ) holds
meet F is closed
proof
let GX be TopSpace; ::_thesis: for F being Subset-Family of GX st ( for A being Subset of GX st A in F holds
A is closed ) holds
meet F is closed
let F be Subset-Family of GX; ::_thesis: ( ( for A being Subset of GX st A in F holds
A is closed ) implies meet F is closed )
assume A1: for A being Subset of GX st A in F holds
A is closed ; ::_thesis: meet F is closed
percases ( F <> {} or F = {} ) ;
supposeA2: F <> {} ; ::_thesis: meet F is closed
defpred S1[ set ] means ([#] GX) \ $1 in F;
consider R1 being Subset-Family of GX such that
A3: for B being Subset of GX holds
( B in R1 iff S1[B] ) from SUBSET_1:sch_3();
A4: for x being set st x in the carrier of GX holds
( ( for A being Subset of GX st A in F holds
x in A ) iff for Z being Subset of GX st Z in R1 holds
not x in Z )
proof
let x be set ; ::_thesis: ( x in the carrier of GX implies ( ( for A being Subset of GX st A in F holds
x in A ) iff for Z being Subset of GX st Z in R1 holds
not x in Z ) )
assume A5: x in the carrier of GX ; ::_thesis: ( ( for A being Subset of GX st A in F holds
x in A ) iff for Z being Subset of GX st Z in R1 holds
not x in Z )
thus  ( ( for A being Subset of GX st A in F holds
x in A ) implies for Z being Subset of GX st Z in R1 holds
not x in Z ) ::_thesis: ( ( for Z being Subset of GX st Z in R1 holds
not x in Z ) implies for A being Subset of GX st A in F holds
x in A )
proof
assume A6: for A being Subset of GX st A in F holds
x in A ; ::_thesis: for Z being Subset of GX st Z in R1 holds
not x in Z
let Z be Subset of GX; ::_thesis: ( Z in R1 implies not x in Z )
assume  Z in R1 ; ::_thesis: not x in Z
then  ([#] GX) \ Z in F by A3;
then  x in ([#] GX) \ Z by A6;
hence  not x in Z by XBOOLE_0:def_5; ::_thesis: verum
end;
assume A7: for Z being Subset of GX st Z in R1 holds
not x in Z ; ::_thesis: for A being Subset of GX st A in F holds
x in A
let A be Subset of GX; ::_thesis: ( A in F implies x in A )
assume A8: A in F ; ::_thesis: x in A
 ([#] GX) \ (([#] GX) \ A) = A by Th3;
then  ([#] GX) \ A in R1 by A3, A8;
then  not x in ([#] GX) \ A by A7;
hence  x in A by A5, XBOOLE_0:def_5; ::_thesis: verum
end;
A9: for x being set holds
( x in ([#] GX) \ (union R1) iff x in meet F )
proof
let x be set ; ::_thesis: ( x in ([#] GX) \ (union R1) iff x in meet F )
thus  ( x in ([#] GX) \ (union R1) implies x in meet F ) ::_thesis: ( x in meet F implies x in ([#] GX) \ (union R1) )
proof
assume A10: x in ([#] GX) \ (union R1) ; ::_thesis: x in meet F
then  not x in union R1 by XBOOLE_0:def_5;
then  for Z being Subset of GX st Z in R1 holds
not x in Z by TARSKI:def_4;
then  for A being set st A in F holds
x in A by A4, A10;
hence  x in meet F by A2, SETFAM_1:def_1; ::_thesis: verum
end;
assume A11: x in meet F ; ::_thesis: x in ([#] GX) \ (union R1)
then  for A being Subset of GX st A in F holds
x in A by SETFAM_1:def_1;
then  for Z being set st x in Z holds
not Z in R1 by A4;
then  not x in union R1 by TARSKI:def_4;
hence  x in ([#] GX) \ (union R1) by A11, XBOOLE_0:def_5; ::_thesis: verum
end;
now__::_thesis:_for_B_being_set_st_B_in_R1_holds_
B_in_the_topology_of_GX
let B be set ; ::_thesis: ( B in R1 implies B in the topology of GX )
assume A12: B in R1 ; ::_thesis: B in the topology of GX
then reconsider B1 = B as Subset of GX ;
 ( B1 in R1 iff ([#] GX) \ B1 in F ) by A3;
then A13: ([#] GX) \ B1 is closed by A1, A12;
 ([#] GX) \ (([#] GX) \ B1) = B1 by Th3;
then  B1 is open by A13, Def3;
hence  B in the topology of GX by Def2; ::_thesis: verum
end;
then  R1 c= the topology of GX by TARSKI:def_3;
then  union R1 in the topology of GX by Def1;
then A14: union R1 is open by Def2;
 ([#] GX) \ (([#] GX) \ (union R1)) = union R1 by Th3;
then  ([#] GX) \ (union R1) is closed by A14, Def3;
hence  meet F is closed by A9, TARSKI:1; ::_thesis: verum
end;
supposeA15: F = {} ; ::_thesis: meet F is closed
 the carrier of GX in the topology of GX by Def1;
then A16: [#] GX is open by Def2;
 [#] GX = ([#] GX) \ ({} GX) ;
then  {} GX is closed by A16, Def3;
hence  meet F is closed by A15, SETFAM_1:def_1; ::_thesis: verum
end;
end;
end;

definition
let GX be TopStruct ;
let A be Subset of GX;
func Cl A ->  Subset of GX means :Def7: :: PRE_TOPC:def 7
 for p being set st p in the carrier of GX holds
( p in it iff for G being Subset of GX st G is open & p in G holds
A meets G );
existence
 ex b1 being Subset of GX st
for p being set st p in the carrier of GX holds
( p in b1 iff for G being Subset of GX st G is open & p in G holds
A meets G )
proof
defpred S1[ set ] means  for G being Subset of GX st G is open & $1 in G holds
A meets G;
consider P being Subset of GX such that
A1: for x being set holds
( x in P iff ( x in the carrier of GX & S1[x] ) ) from SUBSET_1:sch_1();
take  P ; ::_thesis: for p being set st p in the carrier of GX holds
( p in P iff for G being Subset of GX st G is open & p in G holds
A meets G )
thus  for p being set st p in the carrier of GX holds
( p in P iff for G being Subset of GX st G is open & p in G holds
A meets G ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of GX st ( for p being set st p in the carrier of GX holds
( p in b1 iff for G being Subset of GX st G is open & p in G holds
A meets G ) ) & ( for p being set st p in the carrier of GX holds
( p in b2 iff for G being Subset of GX st G is open & p in G holds
A meets G ) ) holds
b1 = b2
proof
let C1, C2 be Subset of GX; ::_thesis: ( ( for p being set st p in the carrier of GX holds
( p in C1 iff for G being Subset of GX st G is open & p in G holds
A meets G ) ) & ( for p being set st p in the carrier of GX holds
( p in C2 iff for G being Subset of GX st G is open & p in G holds
A meets G ) ) implies C1 = C2 )
assume that
A2: for p being set st p in the carrier of GX holds
( p in C1 iff for G being Subset of GX st G is open & p in G holds
A meets G ) and
A3: for p being set st p in the carrier of GX holds
( p in C2 iff for V being Subset of GX st V is open & p in V holds
A meets V ) ; ::_thesis: C1 = C2
 for x being set holds
( x in C1 iff x in C2 )
proof
let x be set ; ::_thesis: ( x in C1 iff x in C2 )
thus  ( x in C1 implies x in C2 ) ::_thesis: ( x in C2 implies x in C1 )
proof
assume A4: x in C1 ; ::_thesis: x in C2
then  for G being Subset of GX st G is open & x in G holds
A meets G by A2;
hence  x in C2 by A3, A4; ::_thesis: verum
end;
assume A5: x in C2 ; ::_thesis: x in C1
then  for V being Subset of GX st V is open & x in V holds
A meets V by A3;
hence  x in C1 by A2, A5; ::_thesis: verum
end;
hence  C1 = C2 by TARSKI:1; ::_thesis: verum
end;
projectivity
 for b1, b2 being Subset of GX st ( for p being set st p in the carrier of GX holds
( p in b1 iff for G being Subset of GX st G is open & p in G holds
b2 meets G ) ) holds
for p being set st p in the carrier of GX holds
( p in b1 iff for G being Subset of GX st G is open & p in G holds
b1 meets G )
proof
let r, A be Subset of GX; ::_thesis: ( ( for p being set st p in the carrier of GX holds
( p in r iff for G being Subset of GX st G is open & p in G holds
A meets G ) ) implies for p being set st p in the carrier of GX holds
( p in r iff for G being Subset of GX st G is open & p in G holds
r meets G ) )
assume A6: for p being set st p in the carrier of GX holds
( p in r iff for G being Subset of GX st G is open & p in G holds
A meets G ) ; ::_thesis: for p being set st p in the carrier of GX holds
( p in r iff for G being Subset of GX st G is open & p in G holds
r meets G )
let p be set ; ::_thesis: ( p in the carrier of GX implies ( p in r iff for G being Subset of GX st G is open & p in G holds
r meets G ) )
assume A7: p in the carrier of GX ; ::_thesis: ( p in r iff for G being Subset of GX st G is open & p in G holds
r meets G )
thus  ( p in r implies for G being Subset of GX st G is open & p in G holds
r meets G ) by XBOOLE_0:3; ::_thesis: ( ( for G being Subset of GX st G is open & p in G holds
r meets G ) implies p in r )
assume A8: for G being Subset of GX st G is open & p in G holds
r meets G ; ::_thesis: p in r
A9: now__::_thesis:_for_C_being_Subset_of_GX_st_C_is_closed_&_A_c=_C_holds_
p_in_C
let C be Subset of GX; ::_thesis: ( C is closed & A c= C implies p in C )
assume  C is closed ; ::_thesis: ( A c= C implies p in C )
then A10: ([#] GX) \ C is open by Def3;
now__::_thesis:_(_p_in_([#]_GX)_\_C_implies_A_meets_([#]_GX)_\_C_)
assume  p in ([#] GX) \ C ; ::_thesis: A meets ([#] GX) \ C
then  r meets ([#] GX) \ C by A8, A10;
then  ex x being set st
( x in r & x in ([#] GX) \ C ) by XBOOLE_0:3;
hence  A meets ([#] GX) \ C by A6, A10; ::_thesis: verum
end;
then  ( not A c= (([#] GX) \ C) ` or p in C or not p in [#] GX ) by SUBSET_1:23, XBOOLE_0:def_5;
hence  ( A c= C implies p in C ) by A7, Th3; ::_thesis: verum
end;
 for G being Subset of GX st G is open & p in G holds
A meets G
proof
let G be Subset of GX; ::_thesis: ( G is open & p in G implies A meets G )
assume A11: G is open ; ::_thesis: ( not p in G or A meets G )
 ([#] GX) \ (([#] GX) \ G) = G by Th3;
then  ([#] GX) \ G is closed by A11, Def3;
then  ( A c= G ` implies p in ([#] GX) \ G ) by A9;
hence  ( not p in G or A meets G ) by SUBSET_1:23, XBOOLE_0:def_5; ::_thesis: verum
end;
hence  p in r by A6, A7; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines Cl PRE_TOPC:def_7_:_
 for GX being TopStruct
for A, b3 being Subset of GX holds
( b3 = Cl A iff for p being set st p in the carrier of GX holds
( p in b3 iff for G being Subset of GX st G is open & p in G holds
A meets G ) );

theorem Th15: :: PRE_TOPC:15
for T being TopStruct
for A being Subset of T
for p being set st p in the carrier of T holds
( p in Cl A iff for C being Subset of T st C is closed & A c= C holds
p in C )
proof
let T be TopStruct ; ::_thesis: for A being Subset of T
for p being set st p in the carrier of T holds
( p in Cl A iff for C being Subset of T st C is closed & A c= C holds
p in C )
let A be Subset of T; ::_thesis: for p being set st p in the carrier of T holds
( p in Cl A iff for C being Subset of T st C is closed & A c= C holds
p in C )
let p be set ; ::_thesis: ( p in the carrier of T implies ( p in Cl A iff for C being Subset of T st C is closed & A c= C holds
p in C ) )
assume A1: p in the carrier of T ; ::_thesis: ( p in Cl A iff for C being Subset of T st C is closed & A c= C holds
p in C )
A2: now__::_thesis:_(_(_for_C_being_Subset_of_T_st_C_is_closed_&_A_c=_C_holds_
p_in_C_)_implies_p_in_Cl_A_)
assume A3: for C being Subset of T st C is closed & A c= C holds
p in C ; ::_thesis: p in Cl A
 for G being Subset of T st G is open & p in G holds
A meets G
proof
let G be Subset of T; ::_thesis: ( G is open & p in G implies A meets G )
assume A4: G is open ; ::_thesis: ( not p in G or A meets G )
 ([#] T) \ (([#] T) \ G) = G by Th3;
then  ([#] T) \ G is closed by A4, Def3;
then  ( A c= G ` implies p in ([#] T) \ G ) by A3;
hence  ( not p in G or A meets G ) by SUBSET_1:23, XBOOLE_0:def_5; ::_thesis: verum
end;
hence  p in Cl A by A1, Def7; ::_thesis: verum
end;
now__::_thesis:_(_p_in_Cl_A_implies_for_C_being_Subset_of_T_st_C_is_closed_&_A_c=_C_holds_
p_in_C_)
assume A5: p in Cl A ; ::_thesis: for C being Subset of T st C is closed & A c= C holds
p in C
let C be Subset of T; ::_thesis: ( C is closed & A c= C implies p in C )
assume  C is closed ; ::_thesis: ( A c= C implies p in C )
then  ([#] T) \ C is open by Def3;
then  ( p in ([#] T) \ C implies A meets ([#] T) \ C ) by A5, Def7;
then  ( not A c= (([#] T) \ C) ` or p in C or not p in [#] T ) by SUBSET_1:23, XBOOLE_0:def_5;
hence  ( A c= C implies p in C ) by A1, Th3; ::_thesis: verum
end;
hence  ( p in Cl A iff for C being Subset of T st C is closed & A c= C holds
p in C ) by A2; ::_thesis: verum
end;

theorem Th16: :: PRE_TOPC:16
for GX being TopSpace
for A being Subset of GX ex F being Subset-Family of GX st
( ( for C being Subset of GX holds
( C in F iff ( C is closed & A c= C ) ) ) & Cl A = meet F )
proof
let GX be TopSpace; ::_thesis: for A being Subset of GX ex F being Subset-Family of GX st
( ( for C being Subset of GX holds
( C in F iff ( C is closed & A c= C ) ) ) & Cl A = meet F )
let A be Subset of GX; ::_thesis: ex F being Subset-Family of GX st
( ( for C being Subset of GX holds
( C in F iff ( C is closed & A c= C ) ) ) & Cl A = meet F )
defpred S1[ set ] means  ex C1 being Subset of GX st
( C1 = $1 & C1 is closed & A c= $1 );
consider F9 being Subset-Family of GX such that
A1: for C being Subset of GX holds
( C in F9 iff S1[C] ) from SUBSET_1:sch_3();
take F = F9; ::_thesis: ( ( for C being Subset of GX holds
( C in F iff ( C is closed & A c= C ) ) ) & Cl A = meet F )
thus  for C being Subset of GX holds
( C in F iff ( C is closed & A c= C ) ) ::_thesis: Cl A = meet F
proof
let C be Subset of GX; ::_thesis: ( C in F iff ( C is closed & A c= C ) )
thus  ( C in F implies ( C is closed & A c= C ) ) ::_thesis: ( C is closed & A c= C implies C in F )
proof
assume  C in F ; ::_thesis: ( C is closed & A c= C )
then  ex C1 being Subset of GX st
( C1 = C & C1 is closed & A c= C ) by A1;
hence  ( C is closed & A c= C ) ; ::_thesis: verum
end;
thus  ( C is closed & A c= C implies C in F ) by A1; ::_thesis: verum
end;
 A c= [#] GX ;
then A2: F <> {} by A1;
 for p being set holds
( p in Cl A iff p in meet F )
proof
let p be set ; ::_thesis: ( p in Cl A iff p in meet F )
A3: now__::_thesis:_(_p_in_meet_F_implies_p_in_Cl_A_)
assume A4: p in meet F ; ::_thesis: p in Cl A
now__::_thesis:_for_C_being_Subset_of_GX_st_C_is_closed_&_A_c=_C_holds_
p_in_C
let C be Subset of GX; ::_thesis: ( C is closed & A c= C implies p in C )
assume  ( C is closed & A c= C ) ; ::_thesis: p in C
then  C in F by A1;
hence  p in C by A4, SETFAM_1:def_1; ::_thesis: verum
end;
hence  p in Cl A by A4, Th15; ::_thesis: verum
end;
now__::_thesis:_(_p_in_Cl_A_implies_p_in_meet_F_)
assume A5: p in Cl A ; ::_thesis: p in meet F
now__::_thesis:_for_C_being_set_st_C_in_F_holds_
p_in_C
let C be set ; ::_thesis: ( C in F implies p in C )
assume  C in F ; ::_thesis: p in C
then  ex C1 being Subset of GX st
( C1 = C & C1 is closed & A c= C ) by A1;
hence  p in C by A5, Th15; ::_thesis: verum
end;
hence  p in meet F by A2, SETFAM_1:def_1; ::_thesis: verum
end;
hence  ( p in Cl A iff p in meet F ) by A3; ::_thesis: verum
end;
hence  Cl A = meet F by TARSKI:1; ::_thesis: verum
end;

theorem :: PRE_TOPC:17
for T being TopStruct
for X9 being SubSpace of T
for A being Subset of T
for A1 being Subset of X9 st A = A1 holds
Cl A1 = (Cl A) /\ ([#] X9)
proof
let T be TopStruct ; ::_thesis: for X9 being SubSpace of T
for A being Subset of T
for A1 being Subset of X9 st A = A1 holds
Cl A1 = (Cl A) /\ ([#] X9)
let X9 be SubSpace of T; ::_thesis: for A being Subset of T
for A1 being Subset of X9 st A = A1 holds
Cl A1 = (Cl A) /\ ([#] X9)
let A be Subset of T; ::_thesis: for A1 being Subset of X9 st A = A1 holds
Cl A1 = (Cl A) /\ ([#] X9)
let A1 be Subset of X9; ::_thesis: ( A = A1 implies Cl A1 = (Cl A) /\ ([#] X9) )
assume A1: A = A1 ; ::_thesis: Cl A1 = (Cl A) /\ ([#] X9)
 for p being set holds
( p in Cl A1 iff p in (Cl A) /\ ([#] X9) )
proof
let p be set ; ::_thesis: ( p in Cl A1 iff p in (Cl A) /\ ([#] X9) )
thus  ( p in Cl A1 implies p in (Cl A) /\ ([#] X9) ) ::_thesis: ( p in (Cl A) /\ ([#] X9) implies p in Cl A1 )
proof
reconsider DD = Cl A1 as Subset of T by Th11;
assume A2: p in Cl A1 ; ::_thesis: p in (Cl A) /\ ([#] X9)
A3: for D1 being Subset of T st D1 is closed & A c= D1 holds
p in D1
proof
let D1 be Subset of T; ::_thesis: ( D1 is closed & A c= D1 implies p in D1 )
assume A4: D1 is closed ; ::_thesis: ( not A c= D1 or p in D1 )
set D3 = D1 /\ ([#] X9);
assume  A c= D1 ; ::_thesis: p in D1
then A5: A1 c= D1 /\ ([#] X9) by A1, XBOOLE_1:19;
 D1 /\ ([#] X9) is closed by A4, Th13;
then  p in D1 /\ ([#] X9) by A2, A5, Th15;
hence  p in D1 by XBOOLE_0:def_4; ::_thesis: verum
end;
 p in DD by A2;
then  p in Cl A by A3, Th15;
hence  p in (Cl A) /\ ([#] X9) by A2, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A6: p in (Cl A) /\ ([#] X9) ; ::_thesis: p in Cl A1
then A7: p in Cl A by XBOOLE_0:def_4;
now__::_thesis:_for_D1_being_Subset_of_X9_st_D1_is_closed_&_A1_c=_D1_holds_
p_in_D1
let D1 be Subset of X9; ::_thesis: ( D1 is closed & A1 c= D1 implies p in D1 )
assume  D1 is closed ; ::_thesis: ( A1 c= D1 implies p in D1 )
then consider D2 being Subset of T such that
A8: D2 is closed and
A9: D1 = D2 /\ ([#] X9) by Th13;
A10: D2 /\ ([#] X9) c= D2 by XBOOLE_1:17;
assume  A1 c= D1 ; ::_thesis: p in D1
then  A c= D2 by A1, A9, A10, XBOOLE_1:1;
then  p in D2 by A7, A8, Th15;
hence  p in D1 by A6, A9, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  p in Cl A1 by A6, Th15; ::_thesis: verum
end;
hence  Cl A1 = (Cl A) /\ ([#] X9) by TARSKI:1; ::_thesis: verum
end;

theorem Th18: :: PRE_TOPC:18
for T being TopStruct
for A being Subset of T holds A c= Cl A
proof
let T be TopStruct ; ::_thesis: for A being Subset of T holds A c= Cl A
let A be Subset of T; ::_thesis: A c= Cl A
now__::_thesis:_for_x_being_set_st_x_in_A_holds_
x_in_Cl_A
let x be set ; ::_thesis: ( x in A implies x in Cl A )
assume A1: x in A ; ::_thesis: x in Cl A
assume  not x in Cl A ; ::_thesis: contradiction
then  ex C being Subset of T st
( C is closed & A c= C & not x in C ) by A1, Th15;
hence  contradiction by A1; ::_thesis: verum
end;
hence  A c= Cl A by TARSKI:def_3; ::_thesis: verum
end;

theorem Th19: :: PRE_TOPC:19
for T being TopStruct
for A, B being Subset of T st A c= B holds
Cl A c= Cl B
proof
let T be TopStruct ; ::_thesis: for A, B being Subset of T st A c= B holds
Cl A c= Cl B
let A, B be Subset of T; ::_thesis: ( A c= B implies Cl A c= Cl B )
assume A1: A c= B ; ::_thesis: Cl A c= Cl B
now__::_thesis:_for_x_being_set_st_x_in_Cl_A_holds_
x_in_Cl_B
let x be set ; ::_thesis: ( x in Cl A implies x in Cl B )
assume A2: x in Cl A ; ::_thesis: x in Cl B
now__::_thesis:_for_D1_being_Subset_of_T_st_D1_is_closed_&_B_c=_D1_holds_
x_in_D1
let D1 be Subset of T; ::_thesis: ( D1 is closed & B c= D1 implies x in D1 )
assume A3: D1 is closed ; ::_thesis: ( B c= D1 implies x in D1 )
assume  B c= D1 ; ::_thesis: x in D1
then  A c= D1 by A1, XBOOLE_1:1;
hence  x in D1 by A2, A3, Th15; ::_thesis: verum
end;
hence  x in Cl B by A2, Th15; ::_thesis: verum
end;
hence  Cl A c= Cl B by TARSKI:def_3; ::_thesis: verum
end;

theorem :: PRE_TOPC:20
for GX being TopSpace
for A, B being Subset of GX holds Cl (A \/ B) = (Cl A) \/ (Cl B)
proof
let GX be TopSpace; ::_thesis: for A, B being Subset of GX holds Cl (A \/ B) = (Cl A) \/ (Cl B)
let A, B be Subset of GX; ::_thesis: Cl (A \/ B) = (Cl A) \/ (Cl B)
now__::_thesis:_for_x_being_set_st_x_in_Cl_(A_\/_B)_holds_
x_in_(Cl_A)_\/_(Cl_B)
let x be set ; ::_thesis: ( x in Cl (A \/ B) implies x in (Cl A) \/ (Cl B) )
assume A1: x in Cl (A \/ B) ; ::_thesis: x in (Cl A) \/ (Cl B)
assume A2: not x in (Cl A) \/ (Cl B) ; ::_thesis: contradiction
then  not x in Cl A by XBOOLE_0:def_3;
then consider G1 being Subset of GX such that
A3: G1 is open and
A4: x in G1 and
A5: A misses G1 by A1, Def7;
A6: A /\ G1 = {} by A5, XBOOLE_0:def_7;
 not x in Cl B by A2, XBOOLE_0:def_3;
then consider G2 being Subset of GX such that
A7: G2 is open and
A8: x in G2 and
A9: B misses G2 by A1, Def7;
A10: G2 in the topology of GX by A7, Def2;
A11: B /\ G2 = {} by A9, XBOOLE_0:def_7;
(A \/ B) /\ (G1 /\ G2) = (A /\ (G1 /\ G2)) \/ (B /\ (G2 /\ G1)) by XBOOLE_1:23
.= ((A /\ G1) /\ G2) \/ (B /\ (G2 /\ G1)) by XBOOLE_1:16
.= {} \/ ({} /\ G1) by A6, A11, XBOOLE_1:16
.= {} GX ;
then A12: A \/ B misses G1 /\ G2 by XBOOLE_0:def_7;
 G1 in the topology of GX by A3, Def2;
then  G1 /\ G2 in the topology of GX by A10, Def1;
then A13: G1 /\ G2 is open by Def2;
 x in G1 /\ G2 by A4, A8, XBOOLE_0:def_4;
hence  contradiction by A1, A13, A12, Def7; ::_thesis: verum
end;
then A14: Cl (A \/ B) c= (Cl A) \/ (Cl B) by TARSKI:def_3;
 ( Cl A c= Cl (A \/ B) & Cl B c= Cl (A \/ B) ) by Th19, XBOOLE_1:7;
then  (Cl A) \/ (Cl B) c= Cl (A \/ B) by XBOOLE_1:8;
hence  Cl (A \/ B) = (Cl A) \/ (Cl B) by A14, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: PRE_TOPC:21
for T being TopStruct
for A, B being Subset of T holds Cl (A /\ B) c= (Cl A) /\ (Cl B)
proof
let T be TopStruct ; ::_thesis: for A, B being Subset of T holds Cl (A /\ B) c= (Cl A) /\ (Cl B)
let A, B be Subset of T; ::_thesis: Cl (A /\ B) c= (Cl A) /\ (Cl B)
 ( Cl (A /\ B) c= Cl A & Cl (A /\ B) c= Cl B ) by Th19, XBOOLE_1:17;
hence  Cl (A /\ B) c= (Cl A) /\ (Cl B) by XBOOLE_1:19; ::_thesis: verum
end;

theorem Th22: :: PRE_TOPC:22
for T being TopStruct
for A being Subset of T holds
( ( A is closed implies Cl A = A ) & ( T is TopSpace-like & Cl A = A implies A is closed ) )
proof
let T be TopStruct ; ::_thesis: for A being Subset of T holds
( ( A is closed implies Cl A = A ) & ( T is TopSpace-like & Cl A = A implies A is closed ) )
let A be Subset of T; ::_thesis: ( ( A is closed implies Cl A = A ) & ( T is TopSpace-like & Cl A = A implies A is closed ) )
thus  ( A is closed implies Cl A = A ) ::_thesis: ( T is TopSpace-like & Cl A = A implies A is closed )
proof
assume  A is closed ; ::_thesis: Cl A = A
then  for x being set st x in Cl A holds
x in A by Th15;
then A1: Cl A c= A by TARSKI:def_3;
 A c= Cl A by Th18;
hence  Cl A = A by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
assume A2: T is TopSpace-like ; ::_thesis: ( not Cl A = A or A is closed )
then consider F being Subset-Family of T such that
A3: for C being Subset of T holds
( C in F iff ( C is closed & A c= C ) ) and
A4: Cl A = meet F by Th16;
assume A5: Cl A = A ; ::_thesis: A is closed
 for C being Subset of T st C in F holds
C is closed by A3;
hence  A is closed by A2, A5, A4, Th14; ::_thesis: verum
end;

theorem :: PRE_TOPC:23
for T being TopStruct
for A being Subset of T holds
( ( A is open implies Cl (([#] T) \ A) = ([#] T) \ A ) & ( T is TopSpace-like & Cl (([#] T) \ A) = ([#] T) \ A implies A is open ) )
proof
let T be TopStruct ; ::_thesis: for A being Subset of T holds
( ( A is open implies Cl (([#] T) \ A) = ([#] T) \ A ) & ( T is TopSpace-like & Cl (([#] T) \ A) = ([#] T) \ A implies A is open ) )
let A be Subset of T; ::_thesis: ( ( A is open implies Cl (([#] T) \ A) = ([#] T) \ A ) & ( T is TopSpace-like & Cl (([#] T) \ A) = ([#] T) \ A implies A is open ) )
 ([#] T) \ (([#] T) \ A) = A by Th3;
then A1: ( A is open iff ([#] T) \ A is closed ) by Def3;
hence  ( A is open implies Cl (([#] T) \ A) = ([#] T) \ A ) by Th22; ::_thesis: ( T is TopSpace-like & Cl (([#] T) \ A) = ([#] T) \ A implies A is open )
assume  ( T is TopSpace-like & Cl (([#] T) \ A) = ([#] T) \ A ) ; ::_thesis: A is open
hence  A is open by A1, Th22; ::_thesis: verum
end;

theorem :: PRE_TOPC:24
for T being TopStruct
for A being Subset of T
for p being Point of T holds
( p in Cl A iff ( not T is empty & ( for G being Subset of T st G is open & p in G holds
A meets G ) ) ) by Def7;

begin

theorem :: PRE_TOPC:25
for T being non empty TopStruct
for A being non empty SubSpace of T
for p being Point of A holds p is Point of T
proof
let T be non empty TopStruct ; ::_thesis: for A being non empty SubSpace of T
for p being Point of A holds p is Point of T
let A be non empty SubSpace of T; ::_thesis: for p being Point of A holds p is Point of T
 [#] A c= [#] T by Def4;
hence  for p being Point of A holds p is Point of T by TARSKI:def_3; ::_thesis: verum
end;

theorem :: PRE_TOPC:26
for A, B, C being TopSpace
for f being Function of A,C st f is continuous & C is SubSpace of B holds
for h being Function of A,B st h = f holds
h is continuous
proof
let A, B, C be TopSpace; ::_thesis: for f being Function of A,C st f is continuous & C is SubSpace of B holds
for h being Function of A,B st h = f holds
h is continuous
let f be Function of A,C; ::_thesis: ( f is continuous & C is SubSpace of B implies for h being Function of A,B st h = f holds
h is continuous )
assume that
A1: f is continuous and
A2: C is SubSpace of B ; ::_thesis: for h being Function of A,B st h = f holds
h is continuous
let h be Function of A,B; ::_thesis: ( h = f implies h is continuous )
assume A3: h = f ; ::_thesis: h is continuous
 for P being Subset of B st P is closed holds
h " P is closed
proof
let P be Subset of B; ::_thesis: ( P is closed implies h " P is closed )
assume A4: P is closed ; ::_thesis: h " P is closed
A5: rng h c= the carrier of C by A3, RELAT_1:def_19;
A6: h " P = h " ((rng h) /\ P) by RELAT_1:133
.= h " (((rng h) /\ ([#] C)) /\ P) by A5, XBOOLE_1:28
.= h " ((rng h) /\ (([#] C) /\ P)) by XBOOLE_1:16
.= h " (P /\ ([#] C)) by RELAT_1:133 ;
reconsider C = C as SubSpace of B by A2;
reconsider Q = P /\ ([#] C) as Subset of C ;
 Q is closed by A4, Th13;
hence  h " P is closed by A1, A3, A6, Def6; ::_thesis: verum
end;
hence  h is continuous by Def6; ::_thesis: verum
end;

theorem :: PRE_TOPC:27
for A being TopSpace
for B being non empty TopSpace
for f being Function of A,B
for C being SubSpace of B st f is continuous holds
for h being Function of A,C st h = f holds
h is continuous
proof
let A be TopSpace; ::_thesis: for B being non empty TopSpace
for f being Function of A,B
for C being SubSpace of B st f is continuous holds
for h being Function of A,C st h = f holds
h is continuous
let B be non empty TopSpace; ::_thesis: for f being Function of A,B
for C being SubSpace of B st f is continuous holds
for h being Function of A,C st h = f holds
h is continuous
let f be Function of A,B; ::_thesis: for C being SubSpace of B st f is continuous holds
for h being Function of A,C st h = f holds
h is continuous
let C be SubSpace of B; ::_thesis: ( f is continuous implies for h being Function of A,C st h = f holds
h is continuous )
assume A1: f is continuous ; ::_thesis: for h being Function of A,C st h = f holds
h is continuous
let h be Function of A,C; ::_thesis: ( h = f implies h is continuous )
assume A2: h = f ; ::_thesis: h is continuous
A3: rng f c= the carrier of C by A2, RELAT_1:def_19;
 for P being Subset of C st P is closed holds
h " P is closed
proof
let P be Subset of C; ::_thesis: ( P is closed implies h " P is closed )
assume  P is closed ; ::_thesis: h " P is closed
then consider Q being Subset of B such that
A4: Q is closed and
A5: Q /\ ([#] C) = P by Th13;
h " P = (f " Q) /\ (f " ([#] C)) by A2, A5, FUNCT_1:68
.= (f " Q) /\ (f " ((rng f) /\ ([#] C))) by RELAT_1:133
.= (f " Q) /\ (f " (rng f)) by A3, XBOOLE_1:28
.= (f " Q) /\ (dom f) by RELAT_1:134
.= f " Q by RELAT_1:132, XBOOLE_1:28 ;
hence  h " P is closed by A1, A4, Def6; ::_thesis: verum
end;
hence  h is continuous by Def6; ::_thesis: verum
end;

registration
let T be TopSpace;
cluster empty  ->  closed for Element of bool the carrier of T;
coherence
 for b1 being Subset of T st b1 is empty holds
b1 is closed
proof
let S be Subset of T; ::_thesis: ( S is empty implies S is closed )
assume  S is empty ; ::_thesis: S is closed
then A1: S = {} T ;
 the carrier of T in the topology of T by Def1;
hence  ([#] T) \ S is open by Def2, A1; :: according to PRE_TOPC:def_3 ::_thesis: verum
end;
end;

registration
let X be TopSpace;
let Y be non empty TopStruct ;
let y be Point of Y;
clusterX --> y ->  continuous ;
coherence
 X --> y is continuous
proof
let P1 be Subset of Y; :: according to PRE_TOPC:def_6 ::_thesis: ( P1 is closed implies (X --> y) " P1 is closed )
assume  P1 is closed ; ::_thesis: (X --> y) " P1 is closed
set F = X --> y;
set H = [#] X;
percases ( y in P1 or not y in P1 ) ;
suppose y in P1 ; ::_thesis: (X --> y) " P1 is closed
then  (X --> y) " P1 = [#] X by FUNCOP_1:14;
hence  (X --> y) " P1 is closed ; ::_thesis: verum
end;
suppose not y in P1 ; ::_thesis: (X --> y) " P1 is closed
then  (X --> y) " P1 = {} X by FUNCOP_1:16;
hence  (X --> y) " P1 is closed ; ::_thesis: verum
end;
end;
end;
end;

registration
let S be TopSpace;
let T be non empty TopSpace;
clusterV7() V10( the carrier of S) V11( the carrier of T) V12() V21( the carrier of S, the carrier of T) continuous for Element of bool [: the carrier of S, the carrier of T:];
existence
 ex b1 being Function of S,T st b1 is continuous
proof
set a = the Point of T;
 S --> the Point of T is continuous ;
hence  ex b1 being Function of S,T st b1 is continuous ; ::_thesis: verum
end;
end;


definition
let T be TopStruct ;
attrT is T_0  means :: PRE_TOPC:def 8
 for x, y being Point of T st ( for G being Subset of T st G is open holds
( x in G iff y in G ) ) holds
x = y;
attrT is T_1  means :Def9: :: PRE_TOPC:def 9
 for p, q being Point of T st p <> q holds
ex G being Subset of T st
( G is open & p in G & q in G ` );
attrT is T_2  means :Def10: :: PRE_TOPC:def 10
 for p, q being Point of T st p <> q holds
ex G1, G2 being Subset of T st
( G1 is open & G2 is open & p in G1 & q in G2 & G1 misses G2 );
attrT is regular  means :: PRE_TOPC:def 11
 for p being Point of T
for F being Subset of T st F is closed & p in F ` holds
ex G1, G2 being Subset of T st
( G1 is open & G2 is open & p in G1 & F c= G2 & G1 misses G2 );
attrT is normal  means :: PRE_TOPC:def 12
 for F1, F2 being Subset of T st F1 is closed & F2 is closed & F1 misses F2 holds
ex G1, G2 being Subset of T st
( G1 is open & G2 is open & F1 c= G1 & F2 c= G2 & G1 misses G2 );
end;

:: deftheorem  defines T_0 PRE_TOPC:def_8_:_
 for T being TopStruct holds
( T is T_0 iff for x, y being Point of T st ( for G being Subset of T st G is open holds
( x in G iff y in G ) ) holds
x = y );

:: deftheorem Def9 defines T_1 PRE_TOPC:def_9_:_
 for T being TopStruct holds
( T is T_1 iff for p, q being Point of T st p <> q holds
ex G being Subset of T st
( G is open & p in G & q in G ` ) );

:: deftheorem Def10 defines T_2 PRE_TOPC:def_10_:_
 for T being TopStruct holds
( T is T_2 iff for p, q being Point of T st p <> q holds
ex G1, G2 being Subset of T st
( G1 is open & G2 is open & p in G1 & q in G2 & G1 misses G2 ) );

:: deftheorem  defines regular PRE_TOPC:def_11_:_
 for T being TopStruct holds
( T is regular iff for p being Point of T
for F being Subset of T st F is closed & p in F ` holds
ex G1, G2 being Subset of T st
( G1 is open & G2 is open & p in G1 & F c= G2 & G1 misses G2 ) );

:: deftheorem  defines normal PRE_TOPC:def_12_:_
 for T being TopStruct holds
( T is normal iff for F1, F2 being Subset of T st F1 is closed & F2 is closed & F1 misses F2 holds
ex G1, G2 being Subset of T st
( G1 is open & G2 is open & F1 c= G1 & F2 c= G2 & G1 misses G2 ) );

definition
let T be TopStruct ;
attrT is T_3  means :Def13: :: PRE_TOPC:def 13
( T is T_1 & T is regular );
attrT is T_4  means :Def14: :: PRE_TOPC:def 14
( T is T_1 & T is normal );
end;

:: deftheorem Def13 defines T_3 PRE_TOPC:def_13_:_
 for T being TopStruct holds
( T is T_3 iff ( T is T_1 & T is regular ) );

:: deftheorem Def14 defines T_4 PRE_TOPC:def_14_:_
 for T being TopStruct holds
( T is T_4 iff ( T is T_1 & T is normal ) );

registration
cluster T_3  ->  T_1 regular for TopStruct ;
coherence
 for b1 being TopStruct st b1 is T_3 holds
( b1 is T_1 & b1 is regular ) by Def13;
cluster T_1 regular  ->  T_3 for TopStruct ;
coherence
 for b1 being TopStruct st b1 is T_1 & b1 is regular holds
b1 is T_3 by Def13;
cluster T_4  ->  T_1 normal for TopStruct ;
coherence
 for b1 being TopStruct st b1 is T_4 holds
( b1 is T_1 & b1 is normal ) by Def14;
cluster T_1 normal  ->  T_4 for TopStruct ;
coherence
 for b1 being TopStruct st b1 is T_1 & b1 is normal holds
b1 is T_4 by Def14;
end;

registration
cluster non empty TopSpace-like T_1 for TopStruct ;
existence
 ex b1 being non empty TopSpace st b1 is T_1
proof
set T = TopStruct(# 1,([#] (bool 1)) #);
A1: ( [#] the carrier of TopStruct(# 1,([#] (bool 1)) #) = the carrier of TopStruct(# 1,([#] (bool 1)) #) & ( for a being Subset-Family of TopStruct(# 1,([#] (bool 1)) #) st a c= the topology of TopStruct(# 1,([#] (bool 1)) #) holds
union a in the topology of TopStruct(# 1,([#] (bool 1)) #) ) ) ;
 for a, b being Subset of TopStruct(# 1,([#] (bool 1)) #) st a in the topology of TopStruct(# 1,([#] (bool 1)) #) & b in the topology of TopStruct(# 1,([#] (bool 1)) #) holds
a /\ b in the topology of TopStruct(# 1,([#] (bool 1)) #) ;
then reconsider T = TopStruct(# 1,([#] (bool 1)) #) as non empty TopSpace by A1, Def1;
take  T ; ::_thesis: T is T_1
let p, q be Point of T; :: according to PRE_TOPC:def_9 ::_thesis: ( p <> q implies ex G being Subset of T st
( G is open & p in G & q in G ` ) )
 p = 0 by CARD_1:49, TARSKI:def_1;
hence  ( p <> q implies ex G being Subset of T st
( G is open & p in G & q in G ` ) ) by CARD_1:49, TARSKI:def_1; ::_thesis: verum
end;
end;

registration
cluster T_1  ->  T_0 for TopStruct ;
coherence
 for b1 being TopStruct st b1 is T_1 holds
b1 is T_0
proof
let T be TopStruct ; ::_thesis: ( T is T_1 implies T is T_0 )
assume A1: T is T_1 ; ::_thesis: T is T_0
let x be Point of T; :: according to PRE_TOPC:def_8 ::_thesis: for y being Point of T st ( for G being Subset of T st G is open holds
( x in G iff y in G ) ) holds
x = y
let y be Point of T; ::_thesis: ( ( for G being Subset of T st G is open holds
( x in G iff y in G ) ) implies x = y )
assume A2: for G being Subset of T st G is open holds
( x in G iff y in G ) ; ::_thesis: x = y
assume  x <> y ; ::_thesis: contradiction
then consider G being Subset of T such that
A3: ( G is open & x in G ) and
A4: y in G ` by A1, Def9;
 not y in G by A4, XBOOLE_0:def_5;
hence  contradiction by A2, A3; ::_thesis: verum
end;
cluster T_2  ->  T_1 for TopStruct ;
coherence
 for b1 being TopStruct st b1 is T_2 holds
b1 is T_1
proof
let T be TopStruct ; ::_thesis: ( T is T_2 implies T is T_1 )
assume A5: T is T_2 ; ::_thesis: T is T_1
let p, q be Point of T; :: according to PRE_TOPC:def_9 ::_thesis: ( p <> q implies ex G being Subset of T st
( G is open & p in G & q in G ` ) )
assume  p <> q ; ::_thesis: ex G being Subset of T st
( G is open & p in G & q in G ` )
then consider G1, G2 being Subset of T such that
A6: G1 is open and
 G2 is open and
A7: p in G1 and
A8: q in G2 and
A9: G1 misses G2 by A5, Def10;
take  G1 ; ::_thesis: ( G1 is open & p in G1 & q in G1 ` )
thus  G1 is open by A6; ::_thesis: ( p in G1 & q in G1 ` )
thus  p in G1 by A7; ::_thesis: q in G1 `
 G2 c= G1 ` by A9, SUBSET_1:23;
hence  q in G1 ` by A8; ::_thesis: verum
end;
end;

registration
let T be TopSpace;
cluster TopStruct(# the carrier of T, the topology of T #) ->  TopSpace-like ;
coherence
 TopStruct(# the carrier of T, the topology of T #) is TopSpace-like
proof
set S = TopStruct(# the carrier of T, the topology of T #);
thus  ( the carrier of TopStruct(# the carrier of T, the topology of T #) in the topology of TopStruct(# the carrier of T, the topology of T #) & ( for a being Subset-Family of TopStruct(# the carrier of T, the topology of T #) st a c= the topology of TopStruct(# the carrier of T, the topology of T #) holds
union a in the topology of TopStruct(# the carrier of T, the topology of T #) ) & ( for a, b being Subset of TopStruct(# the carrier of T, the topology of T #) st a in the topology of TopStruct(# the carrier of T, the topology of T #) & b in the topology of TopStruct(# the carrier of T, the topology of T #) holds
a /\ b in the topology of TopStruct(# the carrier of T, the topology of T #) ) ) by Def1; :: according to PRE_TOPC:def_1 ::_thesis: verum
end;
end;

registration
let T be non empty TopStruct ;
cluster TopStruct(# the carrier of T, the topology of T #) ->  non empty ;
coherence
 not TopStruct(# the carrier of T, the topology of T #) is empty ;
end;

theorem :: PRE_TOPC:28
for T being TopStruct st TopStruct(# the carrier of T, the topology of T #) is TopSpace-like holds
T is TopSpace-like
proof
let T be TopStruct ; ::_thesis: ( TopStruct(# the carrier of T, the topology of T #) is TopSpace-like implies T is TopSpace-like )
set S = TopStruct(# the carrier of T, the topology of T #);
assume  ( the carrier of TopStruct(# the carrier of T, the topology of T #) in the topology of TopStruct(# the carrier of T, the topology of T #) & ( for a being Subset-Family of TopStruct(# the carrier of T, the topology of T #) st a c= the topology of TopStruct(# the carrier of T, the topology of T #) holds
union a in the topology of TopStruct(# the carrier of T, the topology of T #) ) & ( for a, b being Subset of TopStruct(# the carrier of T, the topology of T #) st a in the topology of TopStruct(# the carrier of T, the topology of T #) & b in the topology of TopStruct(# the carrier of T, the topology of T #) holds
a /\ b in the topology of TopStruct(# the carrier of T, the topology of T #) ) ) ; :: according to PRE_TOPC:def_1 ::_thesis: T is TopSpace-like
hence  ( the carrier of T in the topology of T & ( for a being Subset-Family of T st a c= the topology of T holds
union a in the topology of T ) & ( for a, b being Subset of T st a in the topology of T & b in the topology of T holds
a /\ b in the topology of T ) ) ; :: according to PRE_TOPC:def_1 ::_thesis: verum
end;

theorem :: PRE_TOPC:29
for T being TopStruct
for S being SubSpace of TopStruct(# the carrier of T, the topology of T #) holds S is SubSpace of T
proof
let T be TopStruct ; ::_thesis: for S being SubSpace of TopStruct(# the carrier of T, the topology of T #) holds S is SubSpace of T
let S be SubSpace of TopStruct(# the carrier of T, the topology of T #); ::_thesis: S is SubSpace of T
 [#] S c= [#] TopStruct(# the carrier of T, the topology of T #) by Def4;
hence  ( [#] S c= [#] T & ( for P being Subset of S holds
( P in the topology of S iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] S) ) ) ) ) by Def4; :: according to PRE_TOPC:def_4 ::_thesis: verum
end;

registration
let T be TopSpace;
cluster open for Element of bool the carrier of T;
existence
 ex b1 being Subset of T st b1 is open
proof
take  {} T ; ::_thesis: {} T is open
thus  {} T in the topology of T by Th1; :: according to PRE_TOPC:def_2 ::_thesis: verum
end;
end;

theorem :: PRE_TOPC:30
for T being TopSpace
for X being set holds
( X is open Subset of T iff X is open Subset of TopStruct(# the carrier of T, the topology of T #) )
proof
let T be TopSpace; ::_thesis: for X being set holds
( X is open Subset of T iff X is open Subset of TopStruct(# the carrier of T, the topology of T #) )
let X be set ; ::_thesis: ( X is open Subset of T iff X is open Subset of TopStruct(# the carrier of T, the topology of T #) )
 ( X in the topology of T iff X in the topology of TopStruct(# the carrier of T, the topology of T #) ) ;
hence  ( X is open Subset of T iff X is open Subset of TopStruct(# the carrier of T, the topology of T #) ) by Def2; ::_thesis: verum
end;

theorem Th31: :: PRE_TOPC:31
for T being TopSpace
for X being set holds
( X is closed Subset of T iff X is closed Subset of TopStruct(# the carrier of T, the topology of T #) )
proof
let T be TopSpace; ::_thesis: for X being set holds
( X is closed Subset of T iff X is closed Subset of TopStruct(# the carrier of T, the topology of T #) )
let X be set ; ::_thesis: ( X is closed Subset of T iff X is closed Subset of TopStruct(# the carrier of T, the topology of T #) )
 ( ([#] T) \ X in the topology of T iff ([#] TopStruct(# the carrier of T, the topology of T #)) \ X in the topology of TopStruct(# the carrier of T, the topology of T #) ) ;
then  ( ([#] T) \ X is open iff ([#] TopStruct(# the carrier of T, the topology of T #)) \ X is open ) by Def2;
hence  ( X is closed Subset of T iff X is closed Subset of TopStruct(# the carrier of T, the topology of T #) ) by Def3; ::_thesis: verum
end;

theorem Th32: :: PRE_TOPC:32
for S, T being TopSpace
for f being Function of S,T
for g being Function of TopStruct(# the carrier of S, the topology of S #),T st f = g holds
( f is continuous iff g is continuous )
proof
let S, T be TopSpace; ::_thesis: for f being Function of S,T
for g being Function of TopStruct(# the carrier of S, the topology of S #),T st f = g holds
( f is continuous iff g is continuous )
let f be Function of S,T; ::_thesis: for g being Function of TopStruct(# the carrier of S, the topology of S #),T st f = g holds
( f is continuous iff g is continuous )
let g be Function of TopStruct(# the carrier of S, the topology of S #),T; ::_thesis: ( f = g implies ( f is continuous iff g is continuous ) )
assume A1: f = g ; ::_thesis: ( f is continuous iff g is continuous )
thus  ( f is continuous implies g is continuous ) ::_thesis: ( g is continuous implies f is continuous )
proof
assume A2: f is continuous ; ::_thesis: g is continuous
let P1 be Subset of T; :: according to PRE_TOPC:def_6 ::_thesis: ( P1 is closed implies g " P1 is closed )
assume  P1 is closed ; ::_thesis: g " P1 is closed
then  f " P1 is closed by A2, Def6;
hence  g " P1 is closed by A1, Th31; ::_thesis: verum
end;
assume A3: g is continuous ; ::_thesis: f is continuous
let P1 be Subset of T; :: according to PRE_TOPC:def_6 ::_thesis: ( P1 is closed implies f " P1 is closed )
assume  P1 is closed ; ::_thesis: f " P1 is closed
then  g " P1 is closed by A3, Def6;
hence  f " P1 is closed by A1, Th31; ::_thesis: verum
end;

theorem Th33: :: PRE_TOPC:33
for S, T being TopSpace
for f being Function of S,T
for g being Function of S,TopStruct(# the carrier of T, the topology of T #) st f = g holds
( f is continuous iff g is continuous )
proof
let S, T be TopSpace; ::_thesis: for f being Function of S,T
for g being Function of S,TopStruct(# the carrier of T, the topology of T #) st f = g holds
( f is continuous iff g is continuous )
let f be Function of S,T; ::_thesis: for g being Function of S,TopStruct(# the carrier of T, the topology of T #) st f = g holds
( f is continuous iff g is continuous )
let g be Function of S,TopStruct(# the carrier of T, the topology of T #); ::_thesis: ( f = g implies ( f is continuous iff g is continuous ) )
assume A1: f = g ; ::_thesis: ( f is continuous iff g is continuous )
thus  ( f is continuous implies g is continuous ) ::_thesis: ( g is continuous implies f is continuous )
proof
assume A2: f is continuous ; ::_thesis: g is continuous
let P1 be Subset of TopStruct(# the carrier of T, the topology of T #); :: according to PRE_TOPC:def_6 ::_thesis: ( P1 is closed implies g " P1 is closed )
reconsider P = P1 as Subset of T ;
assume  P1 is closed ; ::_thesis: g " P1 is closed
then  P is closed by Th31;
hence  g " P1 is closed by A1, A2, Def6; ::_thesis: verum
end;
assume A3: g is continuous ; ::_thesis: f is continuous
let P1 be Subset of T; :: according to PRE_TOPC:def_6 ::_thesis: ( P1 is closed implies f " P1 is closed )
reconsider P = P1 as Subset of TopStruct(# the carrier of T, the topology of T #) ;
assume  P1 is closed ; ::_thesis: f " P1 is closed
then  P is closed by Th31;
hence  f " P1 is closed by A1, A3, Def6; ::_thesis: verum
end;

theorem :: PRE_TOPC:34
for S, T being TopSpace
for f being Function of S,T
for g being Function of TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #) st f = g holds
( f is continuous iff g is continuous )
proof
let S, T be TopSpace; ::_thesis: for f being Function of S,T
for g being Function of TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #) st f = g holds
( f is continuous iff g is continuous )
let f be Function of S,T; ::_thesis: for g being Function of TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #) st f = g holds
( f is continuous iff g is continuous )
let g be Function of TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #); ::_thesis: ( f = g implies ( f is continuous iff g is continuous ) )
assume A1: f = g ; ::_thesis: ( f is continuous iff g is continuous )
reconsider h = f as Function of S,TopStruct(# the carrier of T, the topology of T #) ;
 ( h is continuous iff g is continuous ) by A1, Th32;
hence  ( f is continuous iff g is continuous ) by Th33; ::_thesis: verum
end;

registration
let T be TopStruct ;
let P be empty Subset of T;
clusterT | P ->  empty strict ;
coherence
 T | P is empty by Th8;
end;

theorem Th35: :: PRE_TOPC:35
for S, T being TopStruct holds
( S is SubSpace of T iff S is SubSpace of TopStruct(# the carrier of T, the topology of T #) )
proof
let S, T be TopStruct ; ::_thesis: ( S is SubSpace of T iff S is SubSpace of TopStruct(# the carrier of T, the topology of T #) )
thus  ( S is SubSpace of T implies S is SubSpace of TopStruct(# the carrier of T, the topology of T #) ) ::_thesis: ( S is SubSpace of TopStruct(# the carrier of T, the topology of T #) implies S is SubSpace of T )
proof
assume A1: S is SubSpace of T ; ::_thesis: S is SubSpace of TopStruct(# the carrier of T, the topology of T #)
then  [#] S c= [#] T by Def4;
hence  [#] S c= [#] TopStruct(# the carrier of T, the topology of T #) ; :: according to PRE_TOPC:def_4 ::_thesis: for P being Subset of S holds
( P in the topology of S iff ex Q being Subset of TopStruct(# the carrier of T, the topology of T #) st
( Q in the topology of TopStruct(# the carrier of T, the topology of T #) & P = Q /\ ([#] S) ) )
let P be Subset of S; ::_thesis: ( P in the topology of S iff ex Q being Subset of TopStruct(# the carrier of T, the topology of T #) st
( Q in the topology of TopStruct(# the carrier of T, the topology of T #) & P = Q /\ ([#] S) ) )
thus  ( P in the topology of S implies ex Q being Subset of TopStruct(# the carrier of T, the topology of T #) st
( Q in the topology of TopStruct(# the carrier of T, the topology of T #) & P = Q /\ ([#] S) ) ) by A1, Def4; ::_thesis: ( ex Q being Subset of TopStruct(# the carrier of T, the topology of T #) st
( Q in the topology of TopStruct(# the carrier of T, the topology of T #) & P = Q /\ ([#] S) ) implies P in the topology of S )
given Q being Subset of TopStruct(# the carrier of T, the topology of T #) such that A2: ( Q in the topology of TopStruct(# the carrier of T, the topology of T #) & P = Q /\ ([#] S) ) ; ::_thesis: P in the topology of S
thus  P in the topology of S by A1, A2, Def4; ::_thesis: verum
end;
assume A3: S is SubSpace of TopStruct(# the carrier of T, the topology of T #) ; ::_thesis: S is SubSpace of T
then  [#] S c= [#] TopStruct(# the carrier of T, the topology of T #) by Def4;
hence  [#] S c= [#] T ; :: according to PRE_TOPC:def_4 ::_thesis: for P being Subset of S holds
( P in the topology of S iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] S) ) )
let P be Subset of S; ::_thesis: ( P in the topology of S iff ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] S) ) )
thus  ( P in the topology of S implies ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] S) ) ) by A3, Def4; ::_thesis: ( ex Q being Subset of T st
( Q in the topology of T & P = Q /\ ([#] S) ) implies P in the topology of S )
given Q being Subset of T such that A4: ( Q in the topology of T & P = Q /\ ([#] S) ) ; ::_thesis: P in the topology of S
thus  P in the topology of S by A3, A4, Def4; ::_thesis: verum
end;

theorem :: PRE_TOPC:36
for T being TopStruct
for X being Subset of T
for Y being Subset of TopStruct(# the carrier of T, the topology of T #) st X = Y holds
TopStruct(# the carrier of (T | X), the topology of (T | X) #) = TopStruct(# the carrier of T, the topology of T #) | Y
proof
let T be TopStruct ; ::_thesis: for X being Subset of T
for Y being Subset of TopStruct(# the carrier of T, the topology of T #) st X = Y holds
TopStruct(# the carrier of (T | X), the topology of (T | X) #) = TopStruct(# the carrier of T, the topology of T #) | Y
let X be Subset of T; ::_thesis: for Y being Subset of TopStruct(# the carrier of T, the topology of T #) st X = Y holds
TopStruct(# the carrier of (T | X), the topology of (T | X) #) = TopStruct(# the carrier of T, the topology of T #) | Y
let Y be Subset of TopStruct(# the carrier of T, the topology of T #); ::_thesis: ( X = Y implies TopStruct(# the carrier of (T | X), the topology of (T | X) #) = TopStruct(# the carrier of T, the topology of T #) | Y )
assume  X = Y ; ::_thesis: TopStruct(# the carrier of (T | X), the topology of (T | X) #) = TopStruct(# the carrier of T, the topology of T #) | Y
then A1: [#] TopStruct(# the carrier of (T | X), the topology of (T | X) #) = Y by Def5;
 TopStruct(# the carrier of (T | X), the topology of (T | X) #) is strict SubSpace of TopStruct(# the carrier of T, the topology of T #) by Th35;
hence  TopStruct(# the carrier of (T | X), the topology of (T | X) #) = TopStruct(# the carrier of T, the topology of T #) | Y by A1, Def5; ::_thesis: verum
end;

registration
cluster empty strict for TopStruct ;
existence
 ex b1 being TopStruct st
( b1 is strict & b1 is empty )
proof
set T = the TopStruct ;
take  the TopStruct | ({} the TopStruct ) ; ::_thesis: ( the TopStruct | ({} the TopStruct ) is strict & the TopStruct | ({} the TopStruct ) is empty )
thus  ( the TopStruct | ({} the TopStruct ) is strict & the TopStruct | ({} the TopStruct ) is empty ) ; ::_thesis: verum
end;
end;

registration
let A be non empty set ;
let t be Subset-Family of A;
cluster TopStruct(# A,t #) ->  non empty ;
coherence
 not TopStruct(# A,t #) is empty ;
end;

registration
cluster empty  ->  T_0 for TopStruct ;
coherence
 for b1 being TopStruct st b1 is empty holds
b1 is T_0
proof
let T be TopStruct ; ::_thesis: ( T is empty implies T is T_0 )
assume A1: T is empty ; ::_thesis: T is T_0
let x, y be Point of T; :: according to PRE_TOPC:def_8 ::_thesis: ( ( for G being Subset of T st G is open holds
( x in G iff y in G ) ) implies x = y )
assume  for G being Subset of T st G is open holds
( x in G iff y in G ) ; ::_thesis: x = y
thus x = {} by A1, SUBSET_1:def_1
.= y by A1, SUBSET_1:def_1 ; ::_thesis: verum
end;
end;

registration
cluster empty strict TopSpace-like for TopStruct ;
existence
 ex b1 being TopSpace st
( b1 is strict & b1 is empty )
proof
set T = the TopSpace;
take  the TopSpace | ({} the TopSpace) ; ::_thesis: ( the TopSpace | ({} the TopSpace) is strict & the TopSpace | ({} the TopSpace) is empty )
thus  ( the TopSpace | ({} the TopSpace) is strict & the TopSpace | ({} the TopSpace) is empty ) ; ::_thesis: verum
end;
end;