:: by Beata Padlewska and Agata Darmochwa\l

::

:: Received April 14, 1989

:: Copyright (c) 1990 Association of Mizar Users

begin

definition

attr c_{1} is strict ;

struct TopStruct -> 1-sorted ;

aggr TopStruct(# carrier, topology #) -> TopStruct ;

sel topology c_{1} -> Subset-Family of the carrier of c_{1};

end;
struct TopStruct -> 1-sorted ;

aggr TopStruct(# carrier, topology #) -> TopStruct ;

sel topology c

definition

let IT be TopStruct ;

attr IT 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;
attr IT 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 ) );

:: 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 TopStruct ;

existence

ex b_{1} being TopStruct st

( not b_{1} is empty & b_{1} is strict & b_{1} is TopSpace-like )

end;
existence

ex b

( not b

proof end;

registration

let T be TopSpace;

cluster the topology of T -> non empty ;

coherence

not the topology of T is empty by Def1;

end;
cluster the topology of T -> non empty ;

coherence

not the topology of T is empty by Def1;

theorem :: PRE_TOPC:1

canceled;

theorem :: PRE_TOPC:2

canceled;

theorem :: PRE_TOPC:3

canceled;

theorem :: PRE_TOPC:4

canceled;

theorem Th5: :: PRE_TOPC:5

proof end;

theorem :: PRE_TOPC:6

canceled;

theorem :: PRE_TOPC:7

canceled;

theorem :: PRE_TOPC:8

canceled;

theorem :: PRE_TOPC:9

canceled;

theorem :: PRE_TOPC:10

canceled;

theorem :: PRE_TOPC:11

canceled;

theorem :: PRE_TOPC:12

canceled;

theorem :: PRE_TOPC:13

canceled;

theorem :: PRE_TOPC:14

canceled;

theorem :: PRE_TOPC:15

canceled;

theorem :: PRE_TOPC:16

canceled;

theorem :: PRE_TOPC:17

canceled;

theorem :: PRE_TOPC:18

proof end;

theorem :: PRE_TOPC:19

canceled;

theorem :: PRE_TOPC:20

canceled;

theorem :: PRE_TOPC:21

canceled;

theorem Th22: :: PRE_TOPC:22

proof end;

theorem Th23: :: PRE_TOPC:23

proof end;

theorem :: PRE_TOPC:24

canceled;

theorem :: PRE_TOPC:25

for T being 1-sorted

for P, Q being Subset of T st [#] T = P \/ Q & P misses Q holds

Q = ([#] T) \ P

for P, Q being Subset of T st [#] T = P \/ Q & P misses Q holds

Q = ([#] T) \ P

proof end;

theorem :: PRE_TOPC:26

canceled;

theorem :: PRE_TOPC:27

definition

let T be TopStruct ;

let P be Subset of T;

canceled;

canceled;

canceled;

attr P is open means :Def5: :: PRE_TOPC:def 5

P in the topology of T;

end;
let P be Subset of T;

canceled;

canceled;

canceled;

attr P is open means :Def5: :: PRE_TOPC:def 5

P in the topology of T;

:: deftheorem PRE_TOPC:def 2 :

canceled;

:: deftheorem PRE_TOPC:def 3 :

canceled;

:: deftheorem PRE_TOPC:def 4 :

canceled;

:: deftheorem Def5 defines open PRE_TOPC:def 5 :

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;

attr P is closed means :Def6: :: PRE_TOPC:def 6

([#] T) \ P is open ;

end;
let P be Subset of T;

attr P is closed means :Def6: :: PRE_TOPC:def 6

([#] T) \ P is open ;

:: deftheorem Def6 defines closed PRE_TOPC:def 6 :

for T being TopStruct

for P being Subset of T holds

( P is closed iff ([#] T) \ P is open );

definition

canceled;

canceled;

let T be TopStruct ;

mode SubSpace of T -> TopStruct means :Def9: :: PRE_TOPC:def 9

( [#] 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 b_{1} being TopStruct st

( [#] b_{1} c= [#] T & ( for P being Subset of b_{1} holds

( P in the topology of b_{1} iff ex Q being Subset of T st

( Q in the topology of T & P = Q /\ ([#] b_{1}) ) ) ) )

end;
canceled;

let T be TopStruct ;

mode SubSpace of T -> TopStruct means :Def9: :: PRE_TOPC:def 9

( [#] 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 b

( [#] b

( P in the topology of b

( Q in the topology of T & P = Q /\ ([#] b

proof end;

:: deftheorem PRE_TOPC:def 7 :

canceled;

:: deftheorem PRE_TOPC:def 8 :

canceled;

:: deftheorem Def9 defines SubSpace PRE_TOPC:def 9 :

for T, b

( b

( P in the topology of b

( Q in the topology of T & P = Q /\ ([#] b

Lm1: for T being TopStruct holds TopStruct(# the carrier of T, the topology of T #) is SubSpace of T

proof end;

registration

let T be TopStruct ;

cluster strict SubSpace of T;

existence

ex b_{1} being SubSpace of T st b_{1} is strict

end;
cluster strict SubSpace of T;

existence

ex b

proof end;

registration

let T be non empty TopStruct ;

cluster non empty strict SubSpace of T;

existence

ex b_{1} being SubSpace of T st

( b_{1} is strict & not b_{1} is empty )

end;
cluster non empty strict SubSpace of T;

existence

ex b

( b

proof end;

registration

let T be TopSpace;

cluster -> TopSpace-like SubSpace of T;

coherence

for b_{1} being SubSpace of T holds b_{1} is TopSpace-like

end;
cluster -> TopSpace-like SubSpace of T;

coherence

for b

proof end;

definition

let T be TopStruct ;

let P be Subset of T;

func T | P -> strict SubSpace of T means :Def10: :: PRE_TOPC:def 10

[#] it = P;

existence

ex b_{1} being strict SubSpace of T st [#] b_{1} = P

for b_{1}, b_{2} being strict SubSpace of T st [#] b_{1} = P & [#] b_{2} = P holds

b_{1} = b_{2}

end;
let P be Subset of T;

func T | P -> strict SubSpace of T means :Def10: :: PRE_TOPC:def 10

[#] it = P;

existence

ex b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def10 defines | PRE_TOPC:def 10 :

for T being TopStruct

for P being Subset of T

for b

( b

registration

let T be non empty TopStruct ;

let P be non empty Subset of T;

cluster T | P -> non empty strict ;

coherence

not T | P is empty

end;
let P be non empty Subset of T;

cluster T | P -> non empty strict ;

coherence

not T | P is empty

proof end;

registration

let T be TopSpace;

cluster strict TopSpace-like SubSpace of T;

existence

ex b_{1} being SubSpace of T st

( b_{1} is TopSpace-like & b_{1} is strict )

end;
cluster strict TopSpace-like SubSpace of T;

existence

ex b

( b

proof end;

registration

let T be TopSpace;

let P be Subset of T;

cluster T | P -> strict TopSpace-like ;

coherence

T | P is TopSpace-like ;

end;
let P be Subset of T;

cluster T | P -> strict TopSpace-like ;

coherence

T | P is TopSpace-like ;

theorem :: PRE_TOPC:28

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

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 end;

theorem Th29: :: PRE_TOPC:29

proof end;

theorem :: PRE_TOPC:30

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

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 end;

definition

let S, T be TopStruct ;

let f be Function of S,T;

canceled;

attr f is continuous means :Def12: :: PRE_TOPC:def 12

for P1 being Subset of T st P1 is closed holds

f " P1 is closed ;

end;
let f be Function of S,T;

canceled;

attr f is continuous means :Def12: :: PRE_TOPC:def 12

for P1 being Subset of T st P1 is closed holds

f " P1 is closed ;

:: deftheorem PRE_TOPC:def 11 :

canceled;

:: deftheorem Def12 defines continuous PRE_TOPC:def 12 :

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:31

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

S2 is SubSpace of T2

proof end;

theorem :: PRE_TOPC:32

canceled;

theorem :: PRE_TOPC:33

canceled;

theorem :: PRE_TOPC:34

canceled;

theorem :: PRE_TOPC:35

canceled;

theorem :: PRE_TOPC:36

canceled;

theorem :: PRE_TOPC:37

canceled;

theorem :: PRE_TOPC:38

canceled;

theorem Th39: :: PRE_TOPC:39

proof end;

theorem :: PRE_TOPC:40

canceled;

theorem :: PRE_TOPC:41

proof end;

registration

let T be TopSpace;

cluster closed Element of bool the carrier of T;

existence

ex b_{1} being Subset of T st b_{1} is closed

end;
cluster closed Element of bool the carrier of T;

existence

ex b

proof end;

registration

let T be non empty TopSpace;

cluster non empty closed Element of bool the carrier of T;

existence

ex b_{1} being Subset of T st

( not b_{1} is empty & b_{1} is closed )

end;
cluster non empty closed Element of bool the carrier of T;

existence

ex b

( not b

proof end;

theorem :: PRE_TOPC:42

canceled;

theorem Th43: :: PRE_TOPC:43

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 ) )

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 end;

theorem Th44: :: PRE_TOPC:44

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

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 end;

definition

let GX be TopStruct ;

let A be Subset of GX;

func Cl A -> Subset of GX means :Def13: :: PRE_TOPC:def 13

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 b_{1} being Subset of GX st

for p being set st p in the carrier of GX holds

( p in b_{1} iff for G being Subset of GX st G is open & p in G holds

A meets G )

for b_{1}, b_{2} being Subset of GX st ( for p being set st p in the carrier of GX holds

( p in b_{1} 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 b_{2} iff for G being Subset of GX st G is open & p in G holds

A meets G ) ) holds

b_{1} = b_{2}

for b_{1}, b_{2} being Subset of GX st ( for p being set st p in the carrier of GX holds

( p in b_{1} iff for G being Subset of GX st G is open & p in G holds

b_{2} meets G ) ) holds

for p being set st p in the carrier of GX holds

( p in b_{1} iff for G being Subset of GX st G is open & p in G holds

b_{1} meets G )

end;
let A be Subset of GX;

func Cl A -> Subset of GX means :Def13: :: PRE_TOPC:def 13

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 b

for p being set st p in the carrier of GX holds

( p in b

A meets G )

proof end;

uniqueness for b

( p in b

A meets G ) ) & ( for p being set st p in the carrier of GX holds

( p in b

A meets G ) ) holds

b

proof end;

projectivity for b

( p in b

b

for p being set st p in the carrier of GX holds

( p in b

b

proof end;

:: deftheorem Def13 defines Cl PRE_TOPC:def 13 :

for GX being TopStruct

for A, b

( b

( p in b

A meets G ) );

theorem Th45: :: PRE_TOPC:45

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 )

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 end;

theorem Th46: :: PRE_TOPC:46

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 )

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 end;

theorem :: PRE_TOPC:47

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)

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 end;

theorem Th48: :: PRE_TOPC:48

proof end;

theorem Th49: :: PRE_TOPC:49

proof end;

theorem :: PRE_TOPC:50

proof end;

theorem :: PRE_TOPC:51

proof end;

theorem Th52: :: PRE_TOPC:52

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 ) )

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 end;

theorem :: PRE_TOPC:53

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 ) )

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 end;

theorem :: PRE_TOPC:54

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 Def13;

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 Def13;

begin

theorem :: PRE_TOPC:55

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

for A being non empty SubSpace of T

for p being Point of A holds p is Point of T

proof end;

theorem :: PRE_TOPC:56

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

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 end;

theorem :: PRE_TOPC:57

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

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 end;

registration

let T be TopSpace;

cluster empty -> closed Element of bool the carrier of T;

coherence

for b_{1} being Subset of T st b_{1} is empty holds

b_{1} is closed

end;
cluster empty -> closed Element of bool the carrier of T;

coherence

for b

b

proof end;

registration

let X be TopSpace;

let Y be non empty TopSpace;

let y be Point of Y;

cluster X --> y -> continuous ;

coherence

X --> y is continuous

end;
let Y be non empty TopSpace;

let y be Point of Y;

cluster X --> y -> continuous ;

coherence

X --> y is continuous

proof end;

registration

let S be TopSpace;

let T be non empty TopSpace;

cluster V7() V10( the carrier of S) V11( the carrier of T) V12() V18( the carrier of S, the carrier of T) continuous Element of bool [: the carrier of S, the carrier of T:];

existence

ex b_{1} being Function of S,T st b_{1} is continuous

end;
let T be non empty TopSpace;

cluster V7() V10( the carrier of S) V11( the carrier of T) V12() V18( the carrier of S, the carrier of T) continuous Element of bool [: the carrier of S, the carrier of T:];

existence

ex b

proof end;

definition

let T be TopStruct ;

attr T is T_0 means :: PRE_TOPC:def 14

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;

attr T is T_1 means :Def15: :: PRE_TOPC:def 15

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 ` );

attr T is T_2 means :Def16: :: PRE_TOPC:def 16

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 );

attr T is regular means :: PRE_TOPC:def 17

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 );

attr T is normal means :: PRE_TOPC:def 18

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;
attr T is T_0 means :: PRE_TOPC:def 14

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;

attr T is T_1 means :Def15: :: PRE_TOPC:def 15

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 ` );

attr T is T_2 means :Def16: :: PRE_TOPC:def 16

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 );

attr T is regular means :: PRE_TOPC:def 17

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 );

attr T is normal means :: PRE_TOPC:def 18

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 );

:: deftheorem defines T_0 PRE_TOPC:def 14 :

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 Def15 defines T_1 PRE_TOPC:def 15 :

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 Def16 defines T_2 PRE_TOPC:def 16 :

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 17 :

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 18 :

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 ;

attr T is T_3 means :Def19: :: PRE_TOPC:def 19

( T is T_1 & T is regular );

attr T is T_4 means :Def20: :: PRE_TOPC:def 20

( T is T_1 & T is normal );

end;
attr T is T_3 means :Def19: :: PRE_TOPC:def 19

( T is T_1 & T is regular );

attr T is T_4 means :Def20: :: PRE_TOPC:def 20

( T is T_1 & T is normal );

:: deftheorem Def19 defines T_3 PRE_TOPC:def 19 :

for T being TopStruct holds

( T is T_3 iff ( T is T_1 & T is regular ) );

:: deftheorem Def20 defines T_4 PRE_TOPC:def 20 :

for T being TopStruct holds

( T is T_4 iff ( T is T_1 & T is normal ) );

registration

cluster T_3 -> T_1 regular TopStruct ;

coherence

for b_{1} being TopStruct st b_{1} is T_3 holds

( b_{1} is T_1 & b_{1} is regular )
by Def19;

cluster T_1 regular -> T_3 TopStruct ;

coherence

for b_{1} being TopStruct st b_{1} is T_1 & b_{1} is regular holds

b_{1} is T_3
by Def19;

cluster T_4 -> T_1 normal TopStruct ;

coherence

for b_{1} being TopStruct st b_{1} is T_4 holds

( b_{1} is T_1 & b_{1} is normal )
by Def20;

cluster T_1 normal -> T_4 TopStruct ;

coherence

for b_{1} being TopStruct st b_{1} is T_1 & b_{1} is normal holds

b_{1} is T_4
by Def20;

end;
coherence

for b

( b

cluster T_1 regular -> T_3 TopStruct ;

coherence

for b

b

cluster T_4 -> T_1 normal TopStruct ;

coherence

for b

( b

cluster T_1 normal -> T_4 TopStruct ;

coherence

for b

b

registration

cluster non empty TopSpace-like T_1 TopStruct ;

existence

ex b_{1} being non empty TopSpace st b_{1} is T_1

end;
existence

ex b

proof end;

registration

cluster T_1 -> T_0 TopStruct ;

coherence

for b_{1} being TopStruct st b_{1} is T_1 holds

b_{1} is T_0

coherence

for b_{1} being TopStruct st b_{1} is T_2 holds

b_{1} is T_1

end;
coherence

for b

b

proof end;

cluster T_2 -> T_1 TopStruct ;coherence

for b

b

proof 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

end;
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 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;
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 ;

theorem :: PRE_TOPC:58

for T being TopStruct st TopStruct(# the carrier of T, the topology of T #) is TopSpace-like holds

T is TopSpace-like

T is TopSpace-like

proof end;

theorem :: PRE_TOPC:59

for T being TopStruct

for S being SubSpace of TopStruct(# the carrier of T, the topology of T #) holds S is SubSpace of T

for S being SubSpace of TopStruct(# the carrier of T, the topology of T #) holds S is SubSpace of T

proof end;

registration

let T be TopSpace;

cluster open Element of bool the carrier of T;

existence

ex b_{1} being Subset of T st b_{1} is open

end;
cluster open Element of bool the carrier of T;

existence

ex b

proof end;

theorem :: PRE_TOPC:60

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 #) )

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 end;

theorem Th61: :: PRE_TOPC:61

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 #) )

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 end;

theorem Th62: :: PRE_TOPC:62

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 )

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 end;

theorem Th63: :: PRE_TOPC:63

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 )

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 end;

theorem :: PRE_TOPC:64

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 )

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 end;

registration

let T be TopStruct ;

let P be empty Subset of T;

cluster T | P -> empty strict ;

coherence

T | P is empty by Th29;

end;
let P be empty Subset of T;

cluster T | P -> empty strict ;

coherence

T | P is empty by Th29;

theorem Th65: :: PRE_TOPC:65

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 #) )

( S is SubSpace of T iff S is SubSpace of TopStruct(# the carrier of T, the topology of T #) )

proof end;

theorem :: PRE_TOPC:66

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

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 end;

registration

cluster empty strict TopStruct ;

existence

ex b_{1} being TopStruct st

( b_{1} is strict & b_{1} is empty )

end;
existence

ex b

( b

proof 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;
let t be Subset-Family of A;

cluster TopStruct(# A,t #) -> non empty ;

coherence

not TopStruct(# A,t #) is empty ;