:: TOPGEN_2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: TOPGEN_2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for B being Basis of T
for x being Element of T holds { U where U is Subset of T : ( x in U & U in B ) } is Basis of x
proof end;

theorem Th2: :: TOPGEN_2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for B being ManySortedSet of T st ( for x being Element of T holds B . x is Basis of x ) holds
Union B is Basis of T
proof end;

definition
let T be non empty TopStruct ;
let x be Element of T;
func Chi x,T -> cardinal number means :Def1: :: TOPGEN_2:def 1
( ex B being Basis of x st it = Card B & ( for B being Basis of x holds it <=` Card B ) );
existence
ex b1 being cardinal number st
( ex B being Basis of x st b1 = Card B & ( for B being Basis of x holds b1 <=` Card B ) )
proof end;
uniqueness
for b1, b2 being cardinal number st ex B being Basis of x st b1 = Card B & ( for B being Basis of x holds b1 <=` Card B ) & ex B being Basis of x st b2 = Card B & ( for B being Basis of x holds b2 <=` Card B ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Chi TOPGEN_2:def 1 :
for T being non empty TopStruct
for x being Element of T
for b3 being cardinal number holds
( b3 = Chi x,T iff ( ex B being Basis of x st b3 = Card B & ( for B being Basis of x holds b3 <=` Card B ) ) );

theorem Th3: :: TOPGEN_2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set st ( for a being set st a in X holds
a is cardinal number ) holds
union X is cardinal number
proof end;

Lm1: now
let T be non empty TopStruct ; :: thesis: ( union { (Chi x,T) where x is Point of T : verum } is cardinal number & ( for m being cardinal number st m = union { (Chi x,T) where x is Point of T : verum } holds
( ( for x being Point of T holds Chi x,T <=` m ) & ( for M being cardinal number st ( for x being Point of T holds Chi x,T <=` M ) holds
m <=` M ) ) ) )

set X = { (Chi x,T) where x is Point of T : verum } ;
now
let a be set ; :: thesis: ( a in { (Chi x,T) where x is Point of T : verum } implies a is cardinal number )
assume a in { (Chi x,T) where x is Point of T : verum } ; :: thesis: a is cardinal number
then ex x being Point of T st a = Chi x,T ;
hence a is cardinal number ; :: thesis: verum
end;
hence union { (Chi x,T) where x is Point of T : verum } is cardinal number by Th3; :: thesis: for m being cardinal number st m = union { (Chi x,T) where x is Point of T : verum } holds
( ( for x being Point of T holds Chi x,T <=` m ) & ( for M being cardinal number st ( for x being Point of T holds Chi x,T <=` M ) holds
m <=` M ) )

let m be cardinal number ; :: thesis: ( m = union { (Chi x,T) where x is Point of T : verum } implies ( ( for x being Point of T holds Chi x,T <=` m ) & ( for M being cardinal number st ( for x being Point of T holds Chi x,T <=` M ) holds
m <=` M ) ) )

assume A1: m = union { (Chi x,T) where x is Point of T : verum } ; :: thesis: ( ( for x being Point of T holds Chi x,T <=` m ) & ( for M being cardinal number st ( for x being Point of T holds Chi x,T <=` M ) holds
m <=` M ) )

hereby :: thesis: for M being cardinal number st ( for x being Point of T holds Chi x,T <=` M ) holds
m <=` M
let x be Point of T; :: thesis: Chi x,T <=` m
Chi x,T in { (Chi x,T) where x is Point of T : verum } ;
hence Chi x,T <=` m by A1, ZFMISC_1:92; :: thesis: verum
end;
let M be cardinal number ; :: thesis: ( ( for x being Point of T holds Chi x,T <=` M ) implies m <=` M )
assume A2: for x being Point of T holds Chi x,T <=` M ; :: thesis: m <=` M
now
let a be set ; :: thesis: ( a in { (Chi x,T) where x is Point of T : verum } implies a c= M )
assume a in { (Chi x,T) where x is Point of T : verum } ; :: thesis: a c= M
then ex x being Point of T st a = Chi x,T ;
hence a c= M by A2; :: thesis: verum
end;
hence m <=` M by A1, ZFMISC_1:94; :: thesis: verum
end;

definition
let T be non empty TopStruct ;
func Chi T -> cardinal number means :Def2: :: TOPGEN_2:def 2
( ( for x being Point of T holds Chi x,T <=` it ) & ( for M being cardinal number st ( for x being Point of T holds Chi x,T <=` M ) holds
it <=` M ) );
existence
ex b1 being cardinal number st
( ( for x being Point of T holds Chi x,T <=` b1 ) & ( for M being cardinal number st ( for x being Point of T holds Chi x,T <=` M ) holds
b1 <=` M ) )
proof end;
uniqueness
for b1, b2 being cardinal number st ( for x being Point of T holds Chi x,T <=` b1 ) & ( for M being cardinal number st ( for x being Point of T holds Chi x,T <=` M ) holds
b1 <=` M ) & ( for x being Point of T holds Chi x,T <=` b2 ) & ( for M being cardinal number st ( for x being Point of T holds Chi x,T <=` M ) holds
b2 <=` M ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Chi TOPGEN_2:def 2 :
for T being non empty TopStruct
for b2 being cardinal number holds
( b2 = Chi T iff ( ( for x being Point of T holds Chi x,T <=` b2 ) & ( for M being cardinal number st ( for x being Point of T holds Chi x,T <=` M ) holds
b2 <=` M ) ) );

theorem Th4: :: TOPGEN_2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopStruct holds Chi T = union { (Chi x,T) where x is Point of T : verum }
proof end;

theorem Th5: :: TOPGEN_2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopStruct
for x being Point of T holds Chi x,T <=` Chi T
proof end;

theorem :: TOPGEN_2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace holds
( T is first-countable iff Chi T <=` alef 0 )
proof end;

definition
let T be non empty TopSpace;
mode Neighborhood_System of T -> ManySortedSet of T means :Def3: :: TOPGEN_2:def 3
for x being Element of T holds it . x is Basis of x;
existence
ex b1 being ManySortedSet of T st
for x being Element of T holds b1 . x is Basis of x
proof end;
end;

:: deftheorem Def3 defines Neighborhood_System TOPGEN_2:def 3 :
for T being non empty TopSpace
for b2 being ManySortedSet of T holds
( b2 is Neighborhood_System of T iff for x being Element of T holds b2 . x is Basis of x );

definition
let T be non empty TopSpace;
let N be Neighborhood_System of T;
:: original: Union
redefine func Union N -> Basis of T;
coherence
Union N is Basis of T
proof end;
let x be Point of T;
:: original: .
redefine func N . x -> Basis of x;
coherence
N . x is Basis of x
by Def3;
end;

theorem :: TOPGEN_2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TOPGEN_2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for x, y being Point of T
for B1 being Basis of x
for B2 being Basis of y
for U being set st x in U & U in B2 holds
ex V being open Subset of T st
( V in B1 & V c= U )
proof end;

theorem :: TOPGEN_2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for x being Point of T
for B being Basis of x
for U1, U2 being set st U1 in B & U2 in B holds
ex V being open Subset of T st
( V in B & V c= U1 /\ U2 )
proof end;

Lm2: now
let T be non empty TopSpace; :: thesis: for A being Subset of T
for x being Element of T st x in Cl A holds
for B being Basis of x
for U being set st U in B holds
U meets A

let A be Subset of T; :: thesis: for x being Element of T st x in Cl A holds
for B being Basis of x
for U being set st U in B holds
U meets A

let x be Element of T; :: thesis: ( x in Cl A implies for B being Basis of x
for U being set st U in B holds
U meets A )

assume A1: x in Cl A ; :: thesis: for B being Basis of x
for U being set st U in B holds
U meets A

let B be Basis of x; :: thesis: for U being set st U in B holds
U meets A

let U be set ; :: thesis: ( U in B implies U meets A )
assume U in B ; :: thesis: U meets A
then A2: ( x in U & U is open Subset of T ) by YELLOW_8:21;
then U meets Cl A by A1, XBOOLE_0:3;
hence U meets A by A2, TSEP_1:40; :: thesis: verum
end;

Lm3: now
let T be non empty TopSpace; :: thesis: for A being Subset of T
for x being Element of T st ex B being Basis of x st
for U being set st U in B holds
U meets A holds
x in Cl A

let A be Subset of T; :: thesis: for x being Element of T st ex B being Basis of x st
for U being set st U in B holds
U meets A holds
x in Cl A

let x be Element of T; :: thesis: ( ex B being Basis of x st
for U being set st U in B holds
U meets A implies x in Cl A )

given B being Basis of x such that A1: for U being set st U in B holds
U meets A ; :: thesis: x in Cl A
now
let U be Subset of T; :: thesis: ( U is open & x in U implies A meets U )
assume ( U is open & x in U ) ; :: thesis: A meets U
then consider V being Subset of T such that
A2: ( V in B & V c= U ) by YELLOW_8:def 2;
V meets A by A1, A2;
hence A meets U by A2, XBOOLE_1:63; :: thesis: verum
end;
hence x in Cl A by PRE_TOPC:def 13; :: thesis: verum
end;

theorem :: TOPGEN_2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for A being Subset of T
for x being Element of T holds
( x in Cl A iff for B being Basis of x
for U being set st U in B holds
U meets A )
proof end;

theorem :: TOPGEN_2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for A being Subset of T
for x being Element of T holds
( x in Cl A iff ex B being Basis of x st
for U being set st U in B holds
U meets A )
proof end;

registration
let T be TopSpace;
cluster non empty open Element of K10(K10(the carrier of T));
existence
ex b1 being Subset-Family of T st
( b1 is open & not b1 is empty )
proof end;
end;

theorem Th12: :: TOPGEN_2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for S being open Subset-Family of T ex G being open Subset-Family of T st
( G c= S & union G = union S & Card G <=` weight T )
proof end;

definition
let T be TopStruct ;
attr T is finite-weight means :Def4: :: TOPGEN_2:def 4
weight T is finite;
end;

:: deftheorem Def4 defines finite-weight TOPGEN_2:def 4 :
for T being TopStruct holds
( T is finite-weight iff weight T is finite );

notation
let T be TopStruct ;
antonym infinite-weight T for finite-weight T;
end;

registration
cluster finite -> finite-weight TopStruct ;
coherence
for b1 being TopStruct st b1 is finite holds
b1 is finite-weight
proof end;
cluster infinite-weight -> infinite TopStruct ;
coherence
for b1 being TopStruct st not b1 is finite-weight holds
not b1 is finite
proof end;
end;

registration
cluster non empty finite finite-weight TopStruct ;
existence
ex b1 being TopSpace st
( b1 is finite & not b1 is empty )
proof end;
end;

theorem Th13: :: TOPGEN_2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds Card (SmallestPartition X) = Card X
proof end;

theorem Th14: :: TOPGEN_2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty discrete TopStruct holds
( SmallestPartition the carrier of T is Basis of T & ( for B being Basis of T holds SmallestPartition the carrier of T c= B ) )
proof end;

theorem Th15: :: TOPGEN_2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty discrete TopStruct holds weight T = Card the carrier of T
proof end;

registration
cluster infinite infinite-weight TopStruct ;
existence
not for b1 being TopSpace holds b1 is finite-weight
proof end;
end;

Lm4: for T being infinite-weight TopSpace
for B being Basis of T ex B1 being Basis of T st
( B1 c= B & Card B1 = weight T )
proof end;

theorem :: TOPGEN_2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th17: :: TOPGEN_2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty finite-weight TopSpace ex B0 being Basis of T ex f being Function of the carrier of T,the topology of T st
( B0 = rng f & ( for x being Point of T holds
( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) ) ) )
proof end;

theorem Th18: :: TOPGEN_2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopSpace
for B0, B being Basis of T
for f being Function of the carrier of T,the topology of T st B0 = rng f & ( for x being Point of T holds
( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) ) ) holds
B0 c= B
proof end;

theorem Th19: :: TOPGEN_2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopSpace
for B0 being Basis of T
for f being Function of the carrier of T,the topology of T st B0 = rng f & ( for x being Point of T holds
( x in f . x & ( for U being open Subset of T st x in U holds
f . x c= U ) ) ) holds
weight T = Card B0
proof end;

Lm5: for T being non empty finite-weight TopSpace
for B being Basis of T ex B1 being Basis of T st
( B1 c= B & Card B1 = weight T )
proof end;

theorem :: TOPGEN_2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for B being Basis of T ex B1 being Basis of T st
( B1 c= B & Card B1 = weight T )
proof end;

definition
let X, x0 be set ;
func DiscrWithInfin X,x0 -> strict TopStruct means :Def5: :: TOPGEN_2:def 5
( the carrier of it = X & the topology of it = { U where U is Subset of X : not x0 in U } \/ { (F ` ) where F is Subset of X : F is finite } );
uniqueness
for b1, b2 being strict TopStruct st the carrier of b1 = X & the topology of b1 = { U where U is Subset of X : not x0 in U } \/ { (F ` ) where F is Subset of X : F is finite } & the carrier of b2 = X & the topology of b2 = { U where U is Subset of X : not x0 in U } \/ { (F ` ) where F is Subset of X : F is finite } holds
b1 = b2
;
existence
ex b1 being strict TopStruct st
( the carrier of b1 = X & the topology of b1 = { U where U is Subset of X : not x0 in U } \/ { (F ` ) where F is Subset of X : F is finite } )
proof end;
end;

:: deftheorem Def5 defines DiscrWithInfin TOPGEN_2:def 5 :
for X, x0 being set
for b3 being strict TopStruct holds
( b3 = DiscrWithInfin X,x0 iff ( the carrier of b3 = X & the topology of b3 = { U where U is Subset of X : not x0 in U } \/ { (F ` ) where F is Subset of X : F is finite } ) );

registration
let X, x0 be set ;
cluster DiscrWithInfin X,x0 -> strict TopSpace-like ;
coherence
DiscrWithInfin X,x0 is TopSpace-like
proof end;
end;

registration
let X be non empty set ;
let x0 be set ;
cluster DiscrWithInfin X,x0 -> non empty strict TopSpace-like ;
coherence
not DiscrWithInfin X,x0 is empty
proof end;
end;

theorem Th21: :: TOPGEN_2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, x0 being set
for A being Subset of (DiscrWithInfin X,x0) holds
( A is open iff ( not x0 in A or A ` is finite ) )
proof end;

theorem Th22: :: TOPGEN_2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, x0 being set
for A being Subset of (DiscrWithInfin X,x0) holds
( A is closed iff not ( x0 in X & not x0 in A & not A is finite ) )
proof end;

theorem :: TOPGEN_2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, x0, x being set st x in X holds
{x} is closed Subset of (DiscrWithInfin X,x0)
proof end;

theorem Th24: :: TOPGEN_2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, x0, x being set st x in X & x <> x0 holds
{x} is open Subset of (DiscrWithInfin X,x0)
proof end;

theorem :: TOPGEN_2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, x0 being set st not X is finite holds
for U being Subset of (DiscrWithInfin X,x0) st U = {x0} holds
not U is open
proof end;

theorem Th26: :: TOPGEN_2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, x0 being set
for A being Subset of (DiscrWithInfin X,x0) st A is finite holds
Cl A = A
proof end;

theorem Th27: :: TOPGEN_2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty TopSpace
for A being Subset of T st not A is closed holds
for a being Point of T st A \/ {a} is closed holds
Cl A = A \/ {a}
proof end;

theorem Th28: :: TOPGEN_2:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, x0 being set st x0 in X holds
for A being Subset of (DiscrWithInfin X,x0) st not A is finite holds
Cl A = A \/ {x0}
proof end;

theorem :: TOPGEN_2:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, x0 being set
for A being Subset of (DiscrWithInfin X,x0) st A ` is finite holds
Int A = A
proof end;

theorem :: TOPGEN_2:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, x0 being set st x0 in X holds
for A being Subset of (DiscrWithInfin X,x0) st not A ` is finite holds
Int A = A \ {x0}
proof end;

theorem Th31: :: TOPGEN_2:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, x0 being set ex B0 being Basis of DiscrWithInfin X,x0 st B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F ` ) where F is Subset of X : F is finite }
proof end;

theorem :: TOPGEN_2:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being infinite set holds Card (Fin X) = Card X
proof end;

theorem Th33: :: TOPGEN_2:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being infinite set holds Card { (F ` ) where F is Subset of X : F is finite } = Card X
proof end;

theorem Th34: :: TOPGEN_2:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being infinite set
for x0 being set
for B0 being Basis of DiscrWithInfin X,x0 st B0 = ((SmallestPartition X) \ {{x0}}) \/ { (F ` ) where F is Subset of X : F is finite } holds
Card B0 = Card X
proof end;

theorem Th35: :: TOPGEN_2:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being infinite set
for x0 being set
for B being Basis of DiscrWithInfin X,x0 holds Card X <=` Card B
proof end;

theorem :: TOPGEN_2:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being infinite set
for x0 being set holds weight (DiscrWithInfin X,x0) = Card X
proof end;

theorem :: TOPGEN_2:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for x0 being set ex B0 being prebasis of DiscrWithInfin X,x0 st B0 = ((SmallestPartition X) \ {{x0}}) \/ { ({x} ` ) where x is Element of X : verum }
proof end;

theorem :: TOPGEN_2:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopSpace
for F being Subset-Family of T
for I being non empty Subset-Family of F st ( for G being set st G in I holds
F \ G is finite ) holds
Cl (union F) = (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } )
proof end;

theorem :: TOPGEN_2:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being TopSpace
for F being Subset-Family of T holds Cl (union F) = (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } )
proof end;

theorem :: TOPGEN_2:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for O being Subset-Family of (bool X) st ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopSpace ) holds
ex B being Subset-Family of X st
( B = Intersect O & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of TopStruct(# X,B #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,o #) is TopExtension of T ) holds
TopStruct(# X,B #) is TopExtension of T ) )
proof end;

theorem :: TOPGEN_2:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for O being Subset-Family of (bool X) ex B being Subset-Family of X st
( B = UniCl (FinMeetCl (union O)) & TopStruct(# X,B #) is TopSpace & ( for o being Subset-Family of X st o in O holds
TopStruct(# X,B #) is TopExtension of TopStruct(# X,o #) ) & ( for T being TopSpace st the carrier of T = X & ( for o being Subset-Family of X st o in O holds
T is TopExtension of TopStruct(# X,o #) ) holds
T is TopExtension of TopStruct(# X,B #) ) )
proof end;