let X be non empty set ; :: thesis: 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; :: thesis: ( ( 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 ; :: thesis: 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; :: thesis: verum