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

then A2: UniCl B = {{}} by YELLOW_9:16;
the carrier of X in Family_open_set X by Th9;
hence ex BB being Subset of B st B1 /\ B2 = union BB by A1, A2, TARSKI:def 1; :: thesis: verum

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 A1, CANTOR_1:def 1;
thus the carrier of X c= union B by A5, ZFMISC_1:77; :: according to XBOOLE_0:def 10 :: thesis: union B c= the carrier of X
thus union B c= the carrier of X ; :: thesis: verum