:: by Zbigniew Karno

::

:: Received July 26, 1994

:: Copyright (c) 1994-2018 Association of Mizar Users

:: 1. Subspaces.

definition

let Y be TopStruct ;

for b_{1} being TopStruct holds

( b_{1} is SubSpace of Y iff ( the carrier of b_{1} c= the carrier of Y & ( for G0 being Subset of b_{1} holds

( G0 is open iff ex G being Subset of Y st

( G is open & G0 = G /\ the carrier of b_{1} ) ) ) ) )

end;
redefine mode SubSpace of Y means :Def1: :: TSP_1:def 1

( the carrier of it c= the carrier of Y & ( for G0 being Subset of it holds

( G0 is open iff ex G being Subset of Y st

( G is open & G0 = G /\ the carrier of it ) ) ) );

compatibility ( the carrier of it c= the carrier of Y & ( for G0 being Subset of it holds

( G0 is open iff ex G being Subset of Y st

( G is open & G0 = G /\ the carrier of it ) ) ) );

for b

( b

( G0 is open iff ex G being Subset of Y st

( G is open & G0 = G /\ the carrier of b

proof end;

:: deftheorem Def1 defines SubSpace TSP_1:def 1 :

for Y, b_{2} being TopStruct holds

( b_{2} is SubSpace of Y iff ( the carrier of b_{2} c= the carrier of Y & ( for G0 being Subset of b_{2} holds

( G0 is open iff ex G being Subset of Y st

( G is open & G0 = G /\ the carrier of b_{2} ) ) ) ) );

for Y, b

( b

( G0 is open iff ex G being Subset of Y st

( G is open & G0 = G /\ the carrier of b

theorem Th1: :: TSP_1:1

for Y being TopStruct

for Y0 being SubSpace of Y

for G being Subset of Y st G is open holds

ex G0 being Subset of Y0 st

( G0 is open & G0 = G /\ the carrier of Y0 )

for Y0 being SubSpace of Y

for G being Subset of Y st G is open holds

ex G0 being Subset of Y0 st

( G0 is open & G0 = G /\ the carrier of Y0 )

proof end;

definition

let Y be TopStruct ;

for b_{1} being TopStruct holds

( b_{1} is SubSpace of Y iff ( the carrier of b_{1} c= the carrier of Y & ( for F0 being Subset of b_{1} holds

( F0 is closed iff ex F being Subset of Y st

( F is closed & F0 = F /\ the carrier of b_{1} ) ) ) ) )

end;
redefine mode SubSpace of Y means :Def2: :: TSP_1:def 2

( the carrier of it c= the carrier of Y & ( for F0 being Subset of it holds

( F0 is closed iff ex F being Subset of Y st

( F is closed & F0 = F /\ the carrier of it ) ) ) );

compatibility ( the carrier of it c= the carrier of Y & ( for F0 being Subset of it holds

( F0 is closed iff ex F being Subset of Y st

( F is closed & F0 = F /\ the carrier of it ) ) ) );

for b

( b

( F0 is closed iff ex F being Subset of Y st

( F is closed & F0 = F /\ the carrier of b

proof end;

:: deftheorem Def2 defines SubSpace TSP_1:def 2 :

for Y, b_{2} being TopStruct holds

( b_{2} is SubSpace of Y iff ( the carrier of b_{2} c= the carrier of Y & ( for F0 being Subset of b_{2} holds

( F0 is closed iff ex F being Subset of Y st

( F is closed & F0 = F /\ the carrier of b_{2} ) ) ) ) );

for Y, b

( b

( F0 is closed iff ex F being Subset of Y st

( F is closed & F0 = F /\ the carrier of b

theorem Th2: :: TSP_1:2

for Y being TopStruct

for Y0 being SubSpace of Y

for F being Subset of Y st F is closed holds

ex F0 being Subset of Y0 st

( F0 is closed & F0 = F /\ the carrier of Y0 )

for Y0 being SubSpace of Y

for F being Subset of Y st F is closed holds

ex F0 being Subset of Y0 st

( F0 is closed & F0 = F /\ the carrier of Y0 )

proof end;

:: 2. Kolmogorov Spaces.

definition

let T be TopStruct ;

( T is T_0 iff ( T is empty or for x, y being Point of T holds

( not x <> y or ex V being Subset of T st

( V is open & x in V & not y in V ) or ex W being Subset of T st

( W is open & not x in W & y in W ) ) ) )

end;
redefine attr T is T_0 means :: TSP_1:def 3

( T is empty or for x, y being Point of T holds

( not x <> y or ex V being Subset of T st

( V is open & x in V & not y in V ) or ex W being Subset of T st

( W is open & not x in W & y in W ) ) );

compatibility ( T is empty or for x, y being Point of T holds

( not x <> y or ex V being Subset of T st

( V is open & x in V & not y in V ) or ex W being Subset of T st

( W is open & not x in W & y in W ) ) );

( T is T_0 iff ( T is empty or for x, y being Point of T holds

( not x <> y or ex V being Subset of T st

( V is open & x in V & not y in V ) or ex W being Subset of T st

( W is open & not x in W & y in W ) ) ) )

proof end;

:: deftheorem defines T_0 TSP_1:def 3 :

for T being TopStruct holds

( T is T_0 iff ( T is empty or for x, y being Point of T holds

( not x <> y or ex V being Subset of T st

( V is open & x in V & not y in V ) or ex W being Subset of T st

( W is open & not x in W & y in W ) ) ) );

for T being TopStruct holds

( T is T_0 iff ( T is empty or for x, y being Point of T holds

( not x <> y or ex V being Subset of T st

( V is open & x in V & not y in V ) or ex W being Subset of T st

( W is open & not x in W & y in W ) ) ) );

definition

let Y be TopStruct ;

( Y is T_0 iff ( Y is empty or for x, y being Point of Y holds

( not x <> y or ex E being Subset of Y st

( E is closed & x in E & not y in E ) or ex F being Subset of Y st

( F is closed & not x in F & y in F ) ) ) )

end;
redefine attr Y is T_0 means :: TSP_1:def 4

( Y is empty or for x, y being Point of Y holds

( not x <> y or ex E being Subset of Y st

( E is closed & x in E & not y in E ) or ex F being Subset of Y st

( F is closed & not x in F & y in F ) ) );

compatibility ( Y is empty or for x, y being Point of Y holds

( not x <> y or ex E being Subset of Y st

( E is closed & x in E & not y in E ) or ex F being Subset of Y st

( F is closed & not x in F & y in F ) ) );

( Y is T_0 iff ( Y is empty or for x, y being Point of Y holds

( not x <> y or ex E being Subset of Y st

( E is closed & x in E & not y in E ) or ex F being Subset of Y st

( F is closed & not x in F & y in F ) ) ) )

proof end;

:: deftheorem defines T_0 TSP_1:def 4 :

for Y being TopStruct holds

( Y is T_0 iff ( Y is empty or for x, y being Point of Y holds

( not x <> y or ex E being Subset of Y st

( E is closed & x in E & not y in E ) or ex F being Subset of Y st

( F is closed & not x in F & y in F ) ) ) );

for Y being TopStruct holds

( Y is T_0 iff ( Y is empty or for x, y being Point of Y holds

( not x <> y or ex E being Subset of Y st

( E is closed & x in E & not y in E ) or ex F being Subset of Y st

( F is closed & not x in F & y in F ) ) ) );

registration
end;

Lm1: for X being non trivial anti-discrete TopStruct holds not X is T_0

proof end;

registration

existence

ex b_{1} being TopSpace st

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

ex b_{1} being TopSpace st

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

end;
ex b

( b

proof end;

existence ex b

( b

proof end;

registration

coherence

for b_{1} being non empty TopSpace st b_{1} is discrete holds

b_{1} is T_0

for b_{1} being non empty TopSpace st not b_{1} is T_0 holds

not b_{1} is discrete
;

coherence

for b_{1} being non empty TopSpace st b_{1} is anti-discrete & not b_{1} is trivial holds

not b_{1} is T_0
by Lm1;

coherence

for b_{1} being non empty TopSpace st b_{1} is anti-discrete & b_{1} is T_0 holds

b_{1} is trivial
;

coherence

for b_{1} being non empty TopSpace st b_{1} is T_0 & not b_{1} is trivial holds

not b_{1} is anti-discrete
;

end;
for b

b

proof end;

coherence for b

not b

coherence

for b

not b

coherence

for b

b

coherence

for b

not b

Lm2: for X being non empty TopSpace

for x being Point of X holds x in Cl {x}

proof end;

definition

let X be non empty TopSpace;

( X is T_0 iff for x, y being Point of X st x <> y holds

Cl {x} <> Cl {y} )

end;
redefine attr X is T_0 means :: TSP_1:def 5

for x, y being Point of X st x <> y holds

Cl {x} <> Cl {y};

compatibility for x, y being Point of X st x <> y holds

Cl {x} <> Cl {y};

( X is T_0 iff for x, y being Point of X st x <> y holds

Cl {x} <> Cl {y} )

proof end;

:: deftheorem defines T_0 TSP_1:def 5 :

for X being non empty TopSpace holds

( X is T_0 iff for x, y being Point of X st x <> y holds

Cl {x} <> Cl {y} );

for X being non empty TopSpace holds

( X is T_0 iff for x, y being Point of X st x <> y holds

Cl {x} <> Cl {y} );

definition

let X be non empty TopSpace;

( X is T_0 iff for x, y being Point of X holds

( not x <> y or not x in Cl {y} or not y in Cl {x} ) )

end;
redefine attr X is T_0 means :: TSP_1:def 6

for x, y being Point of X holds

( not x <> y or not x in Cl {y} or not y in Cl {x} );

compatibility for x, y being Point of X holds

( not x <> y or not x in Cl {y} or not y in Cl {x} );

( X is T_0 iff for x, y being Point of X holds

( not x <> y or not x in Cl {y} or not y in Cl {x} ) )

proof end;

:: deftheorem defines T_0 TSP_1:def 6 :

for X being non empty TopSpace holds

( X is T_0 iff for x, y being Point of X holds

( not x <> y or not x in Cl {y} or not y in Cl {x} ) );

for X being non empty TopSpace holds

( X is T_0 iff for x, y being Point of X holds

( not x <> y or not x in Cl {y} or not y in Cl {x} ) );

definition

let X be non empty TopSpace;

( X is T_0 iff for x, y being Point of X st x <> y & x in Cl {y} holds

not Cl {y} c= Cl {x} )

end;
redefine attr X is T_0 means :: TSP_1:def 7

for x, y being Point of X st x <> y & x in Cl {y} holds

not Cl {y} c= Cl {x};

compatibility for x, y being Point of X st x <> y & x in Cl {y} holds

not Cl {y} c= Cl {x};

( X is T_0 iff for x, y being Point of X st x <> y & x in Cl {y} holds

not Cl {y} c= Cl {x} )

proof end;

:: deftheorem defines T_0 TSP_1:def 7 :

for X being non empty TopSpace holds

( X is T_0 iff for x, y being Point of X st x <> y & x in Cl {y} holds

not Cl {y} c= Cl {x} );

for X being non empty TopSpace holds

( X is T_0 iff for x, y being Point of X st x <> y & x in Cl {y} holds

not Cl {y} c= Cl {x} );

registration

coherence

for b_{1} being non empty TopSpace st b_{1} is almost_discrete & b_{1} is T_0 holds

b_{1} is discrete

for b_{1} being non empty TopSpace st b_{1} is almost_discrete & not b_{1} is discrete holds

not b_{1} is T_0
;

coherence

for b_{1} being non empty TopSpace st not b_{1} is discrete & b_{1} is T_0 holds

not b_{1} is almost_discrete
;

end;
for b

b

proof end;

coherence for b

not b

coherence

for b

not b

definition

mode Kolmogorov_space is non empty T_0 TopSpace;

mode non-Kolmogorov_space is non empty non T_0 TopSpace;

end;
mode non-Kolmogorov_space is non empty non T_0 TopSpace;

registration

existence

ex b_{1} being Kolmogorov_space st

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

ex b_{1} being non-Kolmogorov_space st

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

end;
ex b

( not b

proof end;

existence ex b

( not b

proof end;

:: 3. T_{0} Subsets.

:: deftheorem defines T_0 TSP_1:def 8 :

for Y being TopStruct

for IT being Subset of Y holds

( IT is T_0 iff for x, y being Point of Y st x in IT & y in IT & x <> y & ( for V being Subset of Y holds

( not V is open or not x in V or y in V ) ) holds

ex W being Subset of Y st

( W is open & not x in W & y in W ) );

for Y being TopStruct

for IT being Subset of Y holds

( IT is T_0 iff for x, y being Point of Y st x in IT & y in IT & x <> y & ( for V being Subset of Y holds

( not V is open or not x in V or y in V ) ) holds

ex W being Subset of Y st

( W is open & not x in W & y in W ) );

definition

let Y be non empty TopStruct ;

let A be Subset of Y;

( A is T_0 iff for x, y being Point of Y st x in A & y in A & x <> y & ( for E being Subset of Y holds

( not E is closed or not x in E or y in E ) ) holds

ex F being Subset of Y st

( F is closed & not x in F & y in F ) )

end;
let A be Subset of Y;

redefine attr A is T_0 means :: TSP_1:def 9

for x, y being Point of Y st x in A & y in A & x <> y & ( for E being Subset of Y holds

( not E is closed or not x in E or y in E ) ) holds

ex F being Subset of Y st

( F is closed & not x in F & y in F );

compatibility for x, y being Point of Y st x in A & y in A & x <> y & ( for E being Subset of Y holds

( not E is closed or not x in E or y in E ) ) holds

ex F being Subset of Y st

( F is closed & not x in F & y in F );

( A is T_0 iff for x, y being Point of Y st x in A & y in A & x <> y & ( for E being Subset of Y holds

( not E is closed or not x in E or y in E ) ) holds

ex F being Subset of Y st

( F is closed & not x in F & y in F ) )

proof end;

:: deftheorem defines T_0 TSP_1:def 9 :

for Y being non empty TopStruct

for A being Subset of Y holds

( A is T_0 iff for x, y being Point of Y st x in A & y in A & x <> y & ( for E being Subset of Y holds

( not E is closed or not x in E or y in E ) ) holds

ex F being Subset of Y st

( F is closed & not x in F & y in F ) );

for Y being non empty TopStruct

for A being Subset of Y holds

( A is T_0 iff for x, y being Point of Y st x in A & y in A & x <> y & ( for E being Subset of Y holds

( not E is closed or not x in E or y in E ) ) holds

ex F being Subset of Y st

( F is closed & not x in F & y in F ) );

theorem :: TSP_1:3

for Y0, Y1 being TopStruct

for D0 being Subset of Y0

for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is T_0 holds

D1 is T_0

for D0 being Subset of Y0

for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is T_0 holds

D1 is T_0

proof end;

theorem Th6: :: TSP_1:6

for Y being non empty TopStruct

for A, B being Subset of Y st ( A is T_0 or B is T_0 ) holds

A /\ B is T_0

for A, B being Subset of Y st ( A is T_0 or B is T_0 ) holds

A /\ B is T_0

proof end;

theorem Th7: :: TSP_1:7

for Y being non empty TopStruct

for A, B being Subset of Y st ( A is open or B is open ) & A is T_0 & B is T_0 holds

A \/ B is T_0

for A, B being Subset of Y st ( A is open or B is open ) & A is T_0 & B is T_0 holds

A \/ B is T_0

proof end;

theorem Th8: :: TSP_1:8

for Y being non empty TopStruct

for A, B being Subset of Y st ( A is closed or B is closed ) & A is T_0 & B is T_0 holds

A \/ B is T_0

for A, B being Subset of Y st ( A is closed or B is closed ) & A is T_0 & B is T_0 holds

A \/ B is T_0

proof end;

theorem :: TSP_1:10

for Y being non empty TopStruct

for A being non empty Subset of Y st A is anti-discrete & not A is trivial holds

not A is T_0

for A being non empty Subset of Y st A is anti-discrete & not A is trivial holds

not A is T_0

proof end;

definition

let X be non empty TopSpace;

let A be Subset of X;

( A is T_0 iff for x, y being Point of X st x in A & y in A & x <> y holds

Cl {x} <> Cl {y} )

end;
let A be Subset of X;

redefine attr A is T_0 means :: TSP_1:def 10

for x, y being Point of X st x in A & y in A & x <> y holds

Cl {x} <> Cl {y};

compatibility for x, y being Point of X st x in A & y in A & x <> y holds

Cl {x} <> Cl {y};

( A is T_0 iff for x, y being Point of X st x in A & y in A & x <> y holds

Cl {x} <> Cl {y} )

proof end;

:: deftheorem defines T_0 TSP_1:def 10 :

for X being non empty TopSpace

for A being Subset of X holds

( A is T_0 iff for x, y being Point of X st x in A & y in A & x <> y holds

Cl {x} <> Cl {y} );

for X being non empty TopSpace

for A being Subset of X holds

( A is T_0 iff for x, y being Point of X st x in A & y in A & x <> y holds

Cl {x} <> Cl {y} );

definition

let X be non empty TopSpace;

let A be Subset of X;

( A is T_0 iff for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds

not y in Cl {x} )

end;
let A be Subset of X;

redefine attr A is T_0 means :: TSP_1:def 11

for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds

not y in Cl {x};

compatibility for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds

not y in Cl {x};

( A is T_0 iff for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds

not y in Cl {x} )

proof end;

:: deftheorem defines T_0 TSP_1:def 11 :

for X being non empty TopSpace

for A being Subset of X holds

( A is T_0 iff for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds

not y in Cl {x} );

for X being non empty TopSpace

for A being Subset of X holds

( A is T_0 iff for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds

not y in Cl {x} );

definition

let X be non empty TopSpace;

let A be Subset of X;

( A is T_0 iff for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds

not Cl {y} c= Cl {x} )

end;
let A be Subset of X;

redefine attr A is T_0 means :: TSP_1:def 12

for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds

not Cl {y} c= Cl {x};

compatibility for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds

not Cl {y} c= Cl {x};

( A is T_0 iff for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds

not Cl {y} c= Cl {x} )

proof end;

:: deftheorem defines T_0 TSP_1:def 12 :

for X being non empty TopSpace

for A being Subset of X holds

( A is T_0 iff for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds

not Cl {y} c= Cl {x} );

for X being non empty TopSpace

for A being Subset of X holds

( A is T_0 iff for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds

not Cl {y} c= Cl {x} );

theorem :: TSP_1:12

:: 4. Kolmogorov Subspaces.

registration

let Y be non empty TopStruct ;

existence

ex b_{1} being SubSpace of Y st

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

end;
existence

ex b

( b

proof end;

Lm3: now :: thesis: for Z being TopStruct

for Z0 being SubSpace of Z holds the carrier of Z0 is Subset of Z

for Z0 being SubSpace of Z holds the carrier of Z0 is Subset of Z

let Z be TopStruct ; :: thesis: for Z0 being SubSpace of Z holds the carrier of Z0 is Subset of Z

let Z0 be SubSpace of Z; :: thesis: the carrier of Z0 is Subset of Z

[#] Z0 c= [#] Z by PRE_TOPC:def 4;

hence the carrier of Z0 is Subset of Z ; :: thesis: verum

end;
let Z0 be SubSpace of Z; :: thesis: the carrier of Z0 is Subset of Z

[#] Z0 c= [#] Z by PRE_TOPC:def 4;

hence the carrier of Z0 is Subset of Z ; :: thesis: verum

definition

let Y be TopStruct ;

let Y0 be SubSpace of Y;

( Y0 is T_0 iff ( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for V being Subset of Y holds

( not V is open or not x in V or y in V ) ) holds

ex W being Subset of Y st

( W is open & not x in W & y in W ) ) )

end;
let Y0 be SubSpace of Y;

:: original: T_0

redefine attr Y0 is T_0 means :: TSP_1:def 13

( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for V being Subset of Y holds

( not V is open or not x in V or y in V ) ) holds

ex W being Subset of Y st

( W is open & not x in W & y in W ) );

compatibility redefine attr Y0 is T_0 means :: TSP_1:def 13

( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for V being Subset of Y holds

( not V is open or not x in V or y in V ) ) holds

ex W being Subset of Y st

( W is open & not x in W & y in W ) );

( Y0 is T_0 iff ( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for V being Subset of Y holds

( not V is open or not x in V or y in V ) ) holds

ex W being Subset of Y st

( W is open & not x in W & y in W ) ) )

proof end;

:: deftheorem defines T_0 TSP_1:def 13 :

for Y being TopStruct

for Y0 being SubSpace of Y holds

( Y0 is T_0 iff ( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for V being Subset of Y holds

( not V is open or not x in V or y in V ) ) holds

ex W being Subset of Y st

( W is open & not x in W & y in W ) ) );

for Y being TopStruct

for Y0 being SubSpace of Y holds

( Y0 is T_0 iff ( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for V being Subset of Y holds

( not V is open or not x in V or y in V ) ) holds

ex W being Subset of Y st

( W is open & not x in W & y in W ) ) );

definition

let Y be TopStruct ;

let Y0 be SubSpace of Y;

( Y0 is T_0 iff ( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for E being Subset of Y holds

( not E is closed or not x in E or y in E ) ) holds

ex F being Subset of Y st

( F is closed & not x in F & y in F ) ) )

end;
let Y0 be SubSpace of Y;

:: original: T_0

redefine attr Y0 is T_0 means :: TSP_1:def 14

( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for E being Subset of Y holds

( not E is closed or not x in E or y in E ) ) holds

ex F being Subset of Y st

( F is closed & not x in F & y in F ) );

compatibility redefine attr Y0 is T_0 means :: TSP_1:def 14

( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for E being Subset of Y holds

( not E is closed or not x in E or y in E ) ) holds

ex F being Subset of Y st

( F is closed & not x in F & y in F ) );

( Y0 is T_0 iff ( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for E being Subset of Y holds

( not E is closed or not x in E or y in E ) ) holds

ex F being Subset of Y st

( F is closed & not x in F & y in F ) ) )

proof end;

:: deftheorem defines T_0 TSP_1:def 14 :

for Y being TopStruct

for Y0 being SubSpace of Y holds

( Y0 is T_0 iff ( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for E being Subset of Y holds

( not E is closed or not x in E or y in E ) ) holds

ex F being Subset of Y st

( F is closed & not x in F & y in F ) ) );

for Y being TopStruct

for Y0 being SubSpace of Y holds

( Y0 is T_0 iff ( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for E being Subset of Y holds

( not E is closed or not x in E or y in E ) ) holds

ex F being Subset of Y st

( F is closed & not x in F & y in F ) ) );

theorem :: TSP_1:14

for Y being non empty TopStruct

for Y0 being non empty SubSpace of Y

for Y1 being non empty V142() SubSpace of Y st Y0 is SubSpace of Y1 holds

Y0 is V142()

for Y0 being non empty SubSpace of Y

for Y1 being non empty V142() SubSpace of Y st Y0 is SubSpace of Y1 holds

Y0 is V142()

proof end;

theorem :: TSP_1:15

for X being non empty TopSpace

for X1 being non empty V142() SubSpace of X

for X2 being non empty SubSpace of X st X1 meets X2 holds

X1 meet X2 is V142()

for X1 being non empty V142() SubSpace of X

for X2 being non empty SubSpace of X st X1 meets X2 holds

X1 meet X2 is V142()

proof end;

theorem :: TSP_1:16

for X being non empty TopSpace

for X1, X2 being non empty V142() SubSpace of X st ( X1 is open or X2 is open ) holds

X1 union X2 is V142()

for X1, X2 being non empty V142() SubSpace of X st ( X1 is open or X2 is open ) holds

X1 union X2 is V142()

proof end;

theorem :: TSP_1:17

for X being non empty TopSpace

for X1, X2 being non empty V142() SubSpace of X st ( X1 is closed or X2 is closed ) holds

X1 union X2 is V142()

for X1, X2 being non empty V142() SubSpace of X st ( X1 is closed or X2 is closed ) holds

X1 union X2 is V142()

proof end;

definition
end;

theorem :: TSP_1:18

for X being non empty TopSpace

for A0 being non empty Subset of X st A0 is T_0 holds

ex X0 being strict Kolmogorov_subspace of X st A0 = the carrier of X0

for A0 being non empty Subset of X st A0 is T_0 holds

ex X0 being strict Kolmogorov_subspace of X st A0 = the carrier of X0

proof end;

registration

let X be non trivial TopSpace;

existence

ex b_{1} being Kolmogorov_subspace of X st

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

end;
existence

ex b

( b

proof end;

registration

let X be Kolmogorov_space;

coherence

for b_{1} being non empty SubSpace of X holds b_{1} is V142()

end;
coherence

for b

proof end;

registration

let X be non-Kolmogorov_space;

coherence

for b_{1} being non empty SubSpace of X st not b_{1} is proper holds

not b_{1} is V142()

for b_{1} being non empty SubSpace of X st b_{1} is V142() holds

b_{1} is proper
;

end;
coherence

for b

not b

proof end;

coherence for b

b

registration

let X be non-Kolmogorov_space;

existence

ex b_{1} being SubSpace of X st

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

end;
existence

ex b

( b

proof end;

definition
end;

theorem :: TSP_1:19

for X being non-Kolmogorov_space

for A0 being Subset of X st not A0 is T_0 holds

ex X0 being strict non-Kolmogorov_subspace of X st A0 = the carrier of X0

for A0 being Subset of X st not A0 is T_0 holds

ex X0 being strict non-Kolmogorov_subspace of X st A0 = the carrier of X0

proof end;