let X be non empty set ; for B being non empty Subset-Family of X st ( for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB ) & X = union B holds
ex ET being FMT_TopSpace st
( the carrier of ET = X & B is Basis of ET )
let B be non empty Subset-Family of X; ( ( for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB ) & X = union B implies ex ET being FMT_TopSpace st
( the carrier of ET = X & B is Basis of ET ) )
assume that
A1:
for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB
and
A2:
X = union B
; ex ET being FMT_TopSpace st
( the carrier of ET = X & B is Basis of ET )
set O = UniCl B;
set T = TopStruct(# X,(UniCl B) #);
TopStruct(# X,(UniCl B) #) is TopSpace
by A1, A2, Th3;
then consider ET being FMT_TopSpace such that
A3:
the carrier of TopStruct(# X,(UniCl B) #) = the carrier of ET
and
A4:
Family_open_set ET = the topology of TopStruct(# X,(UniCl B) #)
by Th12;
reconsider B1 = B as Subset-Family of ET by A3;
A5:
B1 is open
by A4, CANTOR_1:1;
B1 is quasi_basis
by A3, A4;
hence
ex ET being FMT_TopSpace st
( the carrier of ET = X & B is Basis of ET )
by A3, A5; verum