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

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