theorem :: FINTOPO7:22

for X being 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 )