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

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

( ( 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

the carrier of X in Family_open_set X
by Th9;
let B1, B2 be Element of B; :: thesis: ex BB being Subset of B st B1 /\ B2 = union BB

end;per cases
( B is empty or not B is empty )
;

end;

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;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

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;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

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