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

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;