begin
begin
definition
let X,
Y be
TopSpace;
existence
ex b1 being strict TopSpace st
( the carrier of b1 = [: the carrier of X, the carrier of Y:] & the topology of b1 = { (union A) where A is Subset-Family of b1 : A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } } )
uniqueness
for b1, b2 being strict TopSpace st the carrier of b1 = [: the carrier of X, the carrier of Y:] & the topology of b1 = { (union A) where A is Subset-Family of b1 : A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } } & the carrier of b2 = [: the carrier of X, the carrier of Y:] & the topology of b2 = { (union A) where A is Subset-Family of b2 : A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } } holds
b1 = b2
;
end;
begin
Lm1:
for X being non empty TopSpace
for A being Subset of X
for V being a_neighborhood of A ex W being Subset of X st
( W is open & A c= W & W c= V & ( for B being Subset of X st B in TrivDecomp X & B meets W holds
B c= W ) )
begin
Lm2:
for T being TopStruct holds TopStruct(# the carrier of T, the topology of T #) is SubSpace of T
begin
Lm3:
TopSpaceMetr RealSpace = TopStruct(# the carrier of RealSpace,(Family_open_set RealSpace) #)
by PCOMPS_1:def 5;