let X be FMT_TopSpace; :: thesis: for B being Basis of X holds
( ( for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB ) & the carrier of X = union B )

let B be Basis of X; :: thesis: ( ( for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB ) & the carrier of X = union B )
A1: B is quasi_basis ;
thus for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB :: thesis: the carrier of X = union B
proof
let B1, B2 be Element of B; :: thesis: ex BB being Subset of B st B1 /\ B2 = union BB
per cases ( B is empty or not B is empty ) ;
suppose B is empty ; :: thesis: ex BB being Subset of B st B1 /\ B2 = union BB
end;
suppose A3: not B is empty ; :: thesis: ex BB being Subset of B st B1 /\ B2 = union BB
B is open ;
then B c= Family_open_set X ;
then ( B1 in Family_open_set X & B2 in Family_open_set X ) by A3;
then ( B1 /\ B2 in Family_open_set X & B is quasi_basis ) by Th9;
then consider Y being Subset-Family of X such that
A4: ( Y c= B & B1 /\ B2 = union Y ) by CANTOR_1:def 1;
reconsider Y = Y as Subset of B by A4;
thus ex BB being Subset of B st B1 /\ B2 = union BB by A4; :: thesis: verum
end;
end;
end;
the carrier of X in Family_open_set X by Th9;
then consider Y being Subset-Family of X such that
A5: ( Y c= B & the carrier of X = union Y ) by ;
thus the carrier of X c= union B by ; :: according to XBOOLE_0:def 10 :: thesis: union B c= the carrier of X
thus union B c= the carrier of X ; :: thesis: verum