:: by Grzegorz Bancerek

::

:: Received December 10, 2004

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

:: deftheorem defines point-filtered TOPGEN_3:def 1 :

for X being set

for B being Subset-Family of X holds

( B is point-filtered iff for x, U1, U2 being set st U1 in B & U2 in B & x in U1 /\ U2 holds

ex U being Subset of X st

( U in B & x in U & U c= U1 /\ U2 ) );

for X being set

for B being Subset-Family of X holds

( B is point-filtered iff for x, U1, U2 being set st U1 in B & U2 in B & x in U1 /\ U2 holds

ex U being Subset of X st

( U in B & x in U & U c= U1 /\ U2 ) );

::<DSCR monograph="topology" name="condition (B2)"/>

theorem Th1: :: TOPGEN_3:1

for X being set

for B being Subset-Family of X holds

( B is covering iff for x being set st x in X holds

ex U being Subset of X st

( U in B & x in U ) )

for B being Subset-Family of X holds

( B is covering iff for x being set st x in X holds

ex U being Subset of X st

( U in B & x in U ) )

proof end;

::<DSCR monograph="topology" label="1.2.1."/>

theorem Th2: :: TOPGEN_3:2

for X being set

for B being Subset-Family of X st B is point-filtered & B is covering holds

for T being TopStruct st the carrier of T = X & the topology of T = UniCl B holds

( T is TopSpace & B is Basis of T )

for B being Subset-Family of X st B is point-filtered & B is covering holds

for T being TopStruct st the carrier of T = X & the topology of T = UniCl B holds

( T is TopSpace & B is Basis of T )

proof end;

::<DSCR monograph="topology" label="1.2.3."/>

theorem :: TOPGEN_3:3

for X being set

for B being non-empty ManySortedSet of X st rng B c= bool (bool X) & ( for x, U being set st x in X & U in B . x holds

x in U ) & ( for x, y, U being set st x in U & U in B . y & y in X holds

ex V being set st

( V in B . x & V c= U ) ) & ( for x, U1, U2 being set st x in X & U1 in B . x & U2 in B . x holds

ex U being set st

( U in B . x & U c= U1 /\ U2 ) ) holds

ex P being Subset-Family of X st

( P = Union B & ( for T being TopStruct st the carrier of T = X & the topology of T = UniCl P holds

( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds

B is Neighborhood_System of T9 ) ) ) )

for B being non-empty ManySortedSet of X st rng B c= bool (bool X) & ( for x, U being set st x in X & U in B . x holds

x in U ) & ( for x, y, U being set st x in U & U in B . y & y in X holds

ex V being set st

( V in B . x & V c= U ) ) & ( for x, U1, U2 being set st x in X & U1 in B . x & U2 in B . x holds

ex U being set st

( U in B . x & U c= U1 /\ U2 ) ) holds

ex P being Subset-Family of X st

( P = Union B & ( for T being TopStruct st the carrier of T = X & the topology of T = UniCl P holds

( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds

B is Neighborhood_System of T9 ) ) ) )

proof end;

::<DSCR monograph="topology" label="1.2.5."/>

theorem Th4: :: TOPGEN_3:4

for X being set

for F being Subset-Family of X st {} in F & ( for A, B being set st A in F & B in F holds

A \/ B in F ) & ( for G being Subset-Family of X st G c= F holds

Intersect G in F ) holds

for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT F holds

( T is TopSpace & ( for A being Subset of T holds

( A is closed iff A in F ) ) )

for F being Subset-Family of X st {} in F & ( for A, B being set st A in F & B in F holds

A \/ B in F ) & ( for G being Subset-Family of X st G c= F holds

Intersect G in F ) holds

for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT F holds

( T is TopSpace & ( for A being Subset of T holds

( A is closed iff A in F ) ) )

proof end;

scheme :: TOPGEN_3:sch 1

TopDefByClosedPred{ F_{1}() -> set , P_{1}[ set ] } :

TopDefByClosedPred{ F

ex T being strict TopSpace st

( the carrier of T = F_{1}() & ( for A being Subset of T holds

( A is closed iff P_{1}[A] ) ) )

provided( the carrier of T = F

( A is closed iff P

A1:
( P_{1}[ {} ] & P_{1}[F_{1}()] )
and

A2: for A, B being set st P_{1}[A] & P_{1}[B] holds

P_{1}[A \/ B]
and

A3: for G being Subset-Family of F_{1}() st ( for A being set st A in G holds

P_{1}[A] ) holds

P_{1}[ Intersect G]

A2: for A, B being set st P

P

A3: for G being Subset-Family of F

P

P

proof end;

Lm1: for T1, T2 being TopSpace st ( for A being set holds

( A is open Subset of T1 iff A is open Subset of T2 ) ) holds

( the carrier of T1 = the carrier of T2 & the topology of T1 c= the topology of T2 )

proof end;

theorem :: TOPGEN_3:5

for T1, T2 being TopSpace st ( for A being set holds

( A is open Subset of T1 iff A is open Subset of T2 ) ) holds

TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #)

( A is open Subset of T1 iff A is open Subset of T2 ) ) holds

TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #)

proof end;

Lm2: for T1, T2 being TopSpace st ( for A being set holds

( A is closed Subset of T1 iff A is closed Subset of T2 ) ) holds

( the carrier of T1 = the carrier of T2 & the topology of T1 c= the topology of T2 )

proof end;

theorem Th6: :: TOPGEN_3:6

for T1, T2 being TopSpace st ( for A being set holds

( A is closed Subset of T1 iff A is closed Subset of T2 ) ) holds

TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #)

( A is closed Subset of T1 iff A is closed Subset of T2 ) ) holds

TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #)

proof end;

definition

let X, Y be set ;

let r be Subset of [:X,(bool Y):];

:: original: rng

redefine func rng r -> Subset-Family of Y;

coherence

rng r is Subset-Family of Y by RELAT_1:def 19;

end;
let r be Subset of [:X,(bool Y):];

:: original: rng

redefine func rng r -> Subset-Family of Y;

coherence

rng r is Subset-Family of Y by RELAT_1:def 19;

::<DSCR monograph="topology" label="1.2.7."/>

theorem Th7: :: TOPGEN_3:7

for X being set

for c being Function of (bool X),(bool X) st c . {} = {} & ( for A being Subset of X holds A c= c . A ) & ( for A, B being Subset of X holds c . (A \/ B) = (c . A) \/ (c . B) ) & ( for A being Subset of X holds c . (c . A) = c . A ) holds

for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT (rng c) holds

( T is TopSpace & ( for A being Subset of T holds Cl A = c . A ) )

for c being Function of (bool X),(bool X) st c . {} = {} & ( for A being Subset of X holds A c= c . A ) & ( for A, B being Subset of X holds c . (A \/ B) = (c . A) \/ (c . B) ) & ( for A being Subset of X holds c . (c . A) = c . A ) holds

for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT (rng c) holds

( T is TopSpace & ( for A being Subset of T holds Cl A = c . A ) )

proof end;

scheme :: TOPGEN_3:sch 2

TopDefByClosureOp{ F_{1}() -> set , F_{2}( object ) -> set } :

TopDefByClosureOp{ F

ex T being strict TopSpace st

( the carrier of T = F_{1}() & ( for A being Subset of T holds Cl A = F_{2}(A) ) )

provided( the carrier of T = F

A1:
F_{2}({}) = {}
and

A2: for A being Subset of F_{1}() holds

( A c= F_{2}(A) & F_{2}(A) c= F_{1}() )
and

A3: for A, B being Subset of F_{1}() holds F_{2}((A \/ B)) = F_{2}(A) \/ F_{2}(B)
and

A4: for A being Subset of F_{1}() holds F_{2}(F_{2}(A)) = F_{2}(A)

A2: for A being Subset of F

( A c= F

A3: for A, B being Subset of F

A4: for A being Subset of F

proof end;

theorem Th8: :: TOPGEN_3:8

for T1, T2 being TopSpace st the carrier of T1 = the carrier of T2 & ( for A1 being Subset of T1

for A2 being Subset of T2 st A1 = A2 holds

Cl A1 = Cl A2 ) holds

the topology of T1 = the topology of T2

for A2 being Subset of T2 st A1 = A2 holds

Cl A1 = Cl A2 ) holds

the topology of T1 = the topology of T2

proof end;

::<DSCR monograph="topology" label="1.2.9."/>

theorem Th9: :: TOPGEN_3:9

for X being set

for i being Function of (bool X),(bool X) st i . X = X & ( for A being Subset of X holds i . A c= A ) & ( for A, B being Subset of X holds i . (A /\ B) = (i . A) /\ (i . B) ) & ( for A being Subset of X holds i . (i . A) = i . A ) holds

for T being TopStruct st the carrier of T = X & the topology of T = rng i holds

( T is TopSpace & ( for A being Subset of T holds Int A = i . A ) )

for i being Function of (bool X),(bool X) st i . X = X & ( for A being Subset of X holds i . A c= A ) & ( for A, B being Subset of X holds i . (A /\ B) = (i . A) /\ (i . B) ) & ( for A being Subset of X holds i . (i . A) = i . A ) holds

for T being TopStruct st the carrier of T = X & the topology of T = rng i holds

( T is TopSpace & ( for A being Subset of T holds Int A = i . A ) )

proof end;

scheme :: TOPGEN_3:sch 3

TopDefByInteriorOp{ F_{1}() -> set , F_{2}( object ) -> set } :

TopDefByInteriorOp{ F

ex T being strict TopSpace st

( the carrier of T = F_{1}() & ( for A being Subset of T holds Int A = F_{2}(A) ) )

provided( the carrier of T = F

A1:
F_{2}(F_{1}()) = F_{1}()
and

A2: for A being Subset of F_{1}() holds F_{2}(A) c= A
and

A3: for A, B being Subset of F_{1}() holds F_{2}((A /\ B)) = F_{2}(A) /\ F_{2}(B)
and

A4: for A being Subset of F_{1}() holds F_{2}(F_{2}(A)) = F_{2}(A)

A2: for A being Subset of F

A3: for A, B being Subset of F

A4: for A being Subset of F

proof end;

theorem Th10: :: TOPGEN_3:10

for T1, T2 being TopSpace st the carrier of T1 = the carrier of T2 & ( for A1 being Subset of T1

for A2 being Subset of T2 st A1 = A2 holds

Int A1 = Int A2 ) holds

the topology of T1 = the topology of T2

for A2 being Subset of T2 st A1 = A2 holds

Int A1 = Int A2 ) holds

the topology of T1 = the topology of T2

proof end;

definition

for b_{1}, b_{2} being non empty strict TopSpace st the carrier of b_{1} = REAL & ex B being Subset-Family of REAL st

( the topology of b_{1} = UniCl B & B = { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } ) & the carrier of b_{2} = REAL & ex B being Subset-Family of REAL st

( the topology of b_{2} = UniCl B & B = { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } ) holds

b_{1} = b_{2}
;

existence

ex b_{1} being non empty strict TopSpace st

( the carrier of b_{1} = REAL & ex B being Subset-Family of REAL st

( the topology of b_{1} = UniCl B & B = { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } ) )
end;

func Sorgenfrey-line -> non empty strict TopSpace means :Def2: :: TOPGEN_3:def 2

( the carrier of it = REAL & ex B being Subset-Family of REAL st

( the topology of it = UniCl B & B = { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } ) );

uniqueness ( the carrier of it = REAL & ex B being Subset-Family of REAL st

( the topology of it = UniCl B & B = { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } ) );

for b

( the topology of b

( the topology of b

b

existence

ex b

( the carrier of b

( the topology of b

proof end;

:: deftheorem Def2 defines Sorgenfrey-line TOPGEN_3:def 2 :

for b_{1} being non empty strict TopSpace holds

( b_{1} = Sorgenfrey-line iff ( the carrier of b_{1} = REAL & ex B being Subset-Family of REAL st

( the topology of b_{1} = UniCl B & B = { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } ) ) );

for b

( b

( the topology of b

Lm3: the carrier of Sorgenfrey-line = REAL

by Def2;

consider BB being Subset-Family of REAL such that

Lm4: the topology of Sorgenfrey-line = UniCl BB and

Lm5: BB = { [.x,q.[ where x, q is Real : ( x < q & q is rational ) } by Def2;

BB c= the topology of Sorgenfrey-line

by Lm4, CANTOR_1:1;

then Lm6: BB is Basis of Sorgenfrey-line

by Lm3, Lm4, CANTOR_1:def 2, TOPS_2:64;

theorem Th18: :: TOPGEN_3:18

for A being set st A is mutually-disjoint & ( for a being set st a in A holds

ex x, y being Real st

( x < y & ].x,y.[ c= a ) ) holds

A is countable

ex x, y being Real st

( x < y & ].x,y.[ c= a ) ) holds

A is countable

proof end;

definition

let X be set ;

let x be Real;

end;
let x be Real;

pred x is_local_minimum_of X means :: TOPGEN_3:def 3

( x in X & ex y being Real st

( y < x & ].y,x.[ misses X ) );

( x in X & ex y being Real st

( y < x & ].y,x.[ misses X ) );

:: deftheorem defines is_local_minimum_of TOPGEN_3:def 3 :

for X being set

for x being Real holds

( x is_local_minimum_of X iff ( x in X & ex y being Real st

( y < x & ].y,x.[ misses X ) ) );

for X being set

for x being Real holds

( x is_local_minimum_of X iff ( x in X & ex y being Real st

( y < x & ].y,x.[ misses X ) ) );

theorem Th19: :: TOPGEN_3:19

for U being Subset of REAL holds { x where x is Element of REAL : x is_local_minimum_of U } is countable

proof end;

registration
end;

definition

let X be set ;

let r be Real;

ex b_{1} being sequence of REAL st

for i being Nat holds

( ( i in X & b_{1} . i = r |^ i ) or ( not i in X & b_{1} . i = 0 ) )

for b_{1}, b_{2} being sequence of REAL st ( for i being Nat holds

( ( i in X & b_{1} . i = r |^ i ) or ( not i in X & b_{1} . i = 0 ) ) ) & ( for i being Nat holds

( ( i in X & b_{2} . i = r |^ i ) or ( not i in X & b_{2} . i = 0 ) ) ) holds

b_{1} = b_{2}

end;
let r be Real;

func X -powers r -> sequence of REAL means :Def5: :: TOPGEN_3:def 5

for i being Nat holds

( ( i in X & it . i = r |^ i ) or ( not i in X & it . i = 0 ) );

existence for i being Nat holds

( ( i in X & it . i = r |^ i ) or ( not i in X & it . i = 0 ) );

ex b

for i being Nat holds

( ( i in X & b

proof end;

uniqueness for b

( ( i in X & b

( ( i in X & b

b

proof end;

:: deftheorem Def5 defines -powers TOPGEN_3:def 5 :

for X being set

for r being Real

for b_{3} being sequence of REAL holds

( b_{3} = X -powers r iff for i being Nat holds

( ( i in X & b_{3} . i = r |^ i ) or ( not i in X & b_{3} . i = 0 ) ) );

for X being set

for r being Real

for b

( b

( ( i in X & b

theorem Th22: :: TOPGEN_3:22

for r being Real

for n being Element of NAT st 0 < r & r < 1 holds

Sum ((r GeoSeq) ^\ n) = (r |^ n) / (1 - r)

for n being Element of NAT st 0 < r & r < 1 holds

Sum ((r GeoSeq) ^\ n) = (r |^ n) / (1 - r)

proof end;

theorem Th25: :: TOPGEN_3:25

for X being set

for n being Element of NAT holds Sum ((X -powers (1 / 2)) ^\ (n + 1)) <= (1 / 2) |^ n

for n being Element of NAT holds Sum ((X -powers (1 / 2)) ^\ (n + 1)) <= (1 / 2) |^ n

proof end;

theorem Th26: :: TOPGEN_3:26

for X being infinite Subset of NAT

for i being Nat holds (Partial_Sums (X -powers (1 / 2))) . i < Sum (X -powers (1 / 2))

for i being Nat holds (Partial_Sums (X -powers (1 / 2))) . i < Sum (X -powers (1 / 2))

proof end;

theorem Th27: :: TOPGEN_3:27

for X, Y being infinite Subset of NAT st Sum (X -powers (1 / 2)) = Sum (Y -powers (1 / 2)) holds

X = Y

X = Y

proof end;

theorem Th31: :: TOPGEN_3:31

for A being Subset-Family of REAL st card A in continuum holds

card { x where x is Element of REAL : ex U being set st

( U in UniCl A & x is_local_minimum_of U ) } in continuum

card { x where x is Element of REAL : ex U being set st

( U in UniCl A & x is_local_minimum_of U ) } in continuum

proof end;

theorem Th32: :: TOPGEN_3:32

for X being Subset-Family of REAL st card X in continuum holds

ex x being Real ex q being Rational st

( x < q & not [.x,q.[ in UniCl X )

ex x being Real ex q being Rational st

( x < q & not [.x,q.[ in UniCl X )

proof end;

definition

let X be set ;

ex b_{1} being strict TopSpace st

( the carrier of b_{1} = X & ( for F being Subset of b_{1} holds

( F is closed iff ( F is finite or F = X ) ) ) )

uniqueness

for b_{1}, b_{2} being strict TopSpace st the carrier of b_{1} = X & ( for F being Subset of b_{1} holds

( F is closed iff ( F is finite or F = X ) ) ) & the carrier of b_{2} = X & ( for F being Subset of b_{2} holds

( F is closed iff ( F is finite or F = X ) ) ) holds

b_{1} = b_{2};

end;
func ClFinTop X -> strict TopSpace means :Def6: :: TOPGEN_3:def 6

( the carrier of it = X & ( for F being Subset of it holds

( F is closed iff ( F is finite or F = X ) ) ) );

existence ( the carrier of it = X & ( for F being Subset of it holds

( F is closed iff ( F is finite or F = X ) ) ) );

ex b

( the carrier of b

( F is closed iff ( F is finite or F = X ) ) ) )

proof end;

correctness uniqueness

for b

( F is closed iff ( F is finite or F = X ) ) ) & the carrier of b

( F is closed iff ( F is finite or F = X ) ) ) holds

b

proof end;

:: deftheorem Def6 defines ClFinTop TOPGEN_3:def 6 :

for X being set

for b_{2} being strict TopSpace holds

( b_{2} = ClFinTop X iff ( the carrier of b_{2} = X & ( for F being Subset of b_{2} holds

( F is closed iff ( F is finite or F = X ) ) ) ) );

for X being set

for b

( b

( F is closed iff ( F is finite or F = X ) ) ) ) );

theorem Th34: :: TOPGEN_3:34

for X being set

for A being Subset of (ClFinTop X) holds

( A is open iff ( A = {} or A ` is finite ) )

for A being Subset of (ClFinTop X) holds

( A is open iff ( A = {} or A ` is finite ) )

proof end;

definition

let X, x0 be set ;

ex b_{1} being strict TopSpace st

( the carrier of b_{1} = X & ( for A being Subset of b_{1} holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X))) ) )

uniqueness

for b_{1}, b_{2} being strict TopSpace st the carrier of b_{1} = X & ( for A being Subset of b_{1} holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X))) ) & the carrier of b_{2} = X & ( for A being Subset of b_{2} holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X))) ) holds

b_{1} = b_{2};

end;
func x0 -PointClTop X -> strict TopSpace means :Def7: :: TOPGEN_3:def 7

( the carrier of it = X & ( for A being Subset of it holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X))) ) );

existence ( the carrier of it = X & ( for A being Subset of it holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X))) ) );

ex b

( the carrier of b

proof end;

correctness uniqueness

for b

b

proof end;

:: deftheorem Def7 defines -PointClTop TOPGEN_3:def 7 :

for X, x0 being set

for b_{3} being strict TopSpace holds

( b_{3} = x0 -PointClTop X iff ( the carrier of b_{3} = X & ( for A being Subset of b_{3} holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X))) ) ) );

for X, x0 being set

for b

( b

registration
end;

theorem Th37: :: TOPGEN_3:37

for X being non empty set

for x0 being Element of X

for A being non empty Subset of (x0 -PointClTop X) holds Cl A = A \/ {x0}

for x0 being Element of X

for A being non empty Subset of (x0 -PointClTop X) holds Cl A = A \/ {x0}

proof end;

theorem Th38: :: TOPGEN_3:38

for X being non empty set

for x0 being Element of X

for A being non empty Subset of (x0 -PointClTop X) holds

( A is closed iff x0 in A )

for x0 being Element of X

for A being non empty Subset of (x0 -PointClTop X) holds

( A is closed iff x0 in A )

proof end;

theorem Th39: :: TOPGEN_3:39

for X being non empty set

for x0 being Element of X

for A being proper Subset of (x0 -PointClTop X) holds

( A is open iff not x0 in A )

for x0 being Element of X

for A being proper Subset of (x0 -PointClTop X) holds

( A is open iff not x0 in A )

proof end;

theorem :: TOPGEN_3:41

for X, x0, x being set st {x0} c< X holds

( {x} is open Subset of (x0 -PointClTop X) iff ( x in X & x <> x0 ) )

( {x} is open Subset of (x0 -PointClTop X) iff ( x in X & x <> x0 ) )

proof end;

definition

let X, X0 be set ;

ex b_{1} being strict TopSpace st

( the carrier of b_{1} = X & ( for A being Subset of b_{1} holds Int A = IFEQ (A,X,A,(A /\ X0)) ) )

uniqueness

for b_{1}, b_{2} being strict TopSpace st the carrier of b_{1} = X & ( for A being Subset of b_{1} holds Int A = IFEQ (A,X,A,(A /\ X0)) ) & the carrier of b_{2} = X & ( for A being Subset of b_{2} holds Int A = IFEQ (A,X,A,(A /\ X0)) ) holds

b_{1} = b_{2};

end;
func X0 -DiscreteTop X -> strict TopSpace means :Def8: :: TOPGEN_3:def 8

( the carrier of it = X & ( for A being Subset of it holds Int A = IFEQ (A,X,A,(A /\ X0)) ) );

existence ( the carrier of it = X & ( for A being Subset of it holds Int A = IFEQ (A,X,A,(A /\ X0)) ) );

ex b

( the carrier of b

proof end;

correctness uniqueness

for b

b

proof end;

:: deftheorem Def8 defines -DiscreteTop TOPGEN_3:def 8 :

for X, X0 being set

for b_{3} being strict TopSpace holds

( b_{3} = X0 -DiscreteTop X iff ( the carrier of b_{3} = X & ( for A being Subset of b_{3} holds Int A = IFEQ (A,X,A,(A /\ X0)) ) ) );

for X, X0 being set

for b

( b

registration
end;

theorem Th42: :: TOPGEN_3:42

for X being non empty set

for X0 being set

for A being proper Subset of (X0 -DiscreteTop X) holds Int A = A /\ X0

for X0 being set

for A being proper Subset of (X0 -DiscreteTop X) holds Int A = A /\ X0

proof end;

theorem Th43: :: TOPGEN_3:43

for X being non empty set

for X0 being set

for A being proper Subset of (X0 -DiscreteTop X) holds

( A is open iff A c= X0 )

for X0 being set

for A being proper Subset of (X0 -DiscreteTop X) holds

( A is open iff A c= X0 )

proof end;

theorem Th44: :: TOPGEN_3:44

for X being set

for X0 being Subset of X holds the topology of (X0 -DiscreteTop X) = {X} \/ (bool X0)

for X0 being Subset of X holds the topology of (X0 -DiscreteTop X) = {X} \/ (bool X0)

proof end;