begin
:: deftheorem Def1 defines SubSpace TSP_1:def 1 :
for Y, b2 being TopStruct holds
( b2 is SubSpace of Y iff ( the carrier of b2 c= the carrier of Y & ( for G0 being Subset of b2 holds
( G0 is open iff ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of b2 ) ) ) ) );
theorem
canceled;
theorem Th2:
:: deftheorem Def2 defines SubSpace TSP_1:def 2 :
for Y, b2 being TopStruct holds
( b2 is SubSpace of Y iff ( the carrier of b2 c= the carrier of Y & ( for F0 being Subset of b2 holds
( F0 is closed iff ex F being Subset of Y st
( F is closed & F0 = F /\ the carrier of b2 ) ) ) ) );
theorem
canceled;
theorem Th4:
begin
:: deftheorem Def3 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 ) ) ) );
:: deftheorem Def4 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 ) ) ) );
Lm1:
for X being non empty non trivial anti-discrete TopStruct holds not X is T_0
Lm2:
for X being non empty TopSpace
for x being Point of X holds x in Cl {x}
:: deftheorem Def5 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} );
:: deftheorem Def6 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} ) );
:: 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} );
begin
:: deftheorem Def8 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 ) );
:: deftheorem Def9 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 ) );
theorem
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem
:: deftheorem Def10 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} );
:: deftheorem Def11 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} );
:: 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} );
theorem Th13:
theorem
begin
:: 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 ) ) );
:: deftheorem Def14 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 ) ) );
theorem Th15:
theorem
theorem
theorem
theorem
theorem
theorem