let X be FMT_TopSpace; :: thesis: for B being Basis of X holds Family_open_set X = UniCl B

let B be Basis of X; :: thesis: Family_open_set X = UniCl B

thus Family_open_set X c= UniCl B by Def8; :: according to XBOOLE_0:def 10 :: thesis: UniCl B c= Family_open_set X

let B be Basis of X; :: thesis: Family_open_set X = UniCl B

thus Family_open_set X c= UniCl B by Def8; :: according to XBOOLE_0:def 10 :: thesis: UniCl B c= Family_open_set X

hereby :: according to TARSKI:def 3 :: thesis: verum

let t be object ; :: thesis: ( t in UniCl B implies t in Family_open_set X )

assume t in UniCl B ; :: thesis: t in Family_open_set X

then consider Y being Subset-Family of X such that

A1: ( Y c= B & t = union Y ) by CANTOR_1:def 1;

B is open ;

then B c= Family_open_set X ;

then Y c= Family_open_set X by A1;

hence t in Family_open_set X by A1, Th9; :: thesis: verum

end;assume t in UniCl B ; :: thesis: t in Family_open_set X

then consider Y being Subset-Family of X such that

A1: ( Y c= B & t = union Y ) by CANTOR_1:def 1;

B is open ;

then B c= Family_open_set X ;

then Y c= Family_open_set X by A1;

hence t in Family_open_set X by A1, Th9; :: thesis: verum