let T be TopSpace; :: thesis: for K being Subset-Family of T holds
( K is prebasis of T iff FinMeetCl K is Basis of T )
let BB be Subset-Family of T; :: thesis: ( BB is prebasis of T iff FinMeetCl BB is Basis of T )

A1: now

assume A2: T is empty ; :: thesis: the topology of T = bool the carrier of T
then the topology of T = {{} } by Th8;
hence the topology of T = bool the carrier of T by A2, ZFMISC_1:1; :: thesis: verum

end;

thus ( BB is prebasis of T implies FinMeetCl BB is Basis of T ) :: thesis: ( FinMeetCl BB is Basis of T implies BB is prebasis of T )

proof

assume A3: BB is prebasis of T ; :: thesis: FinMeetCl BB is Basis of T
then BB c= the topology of T by TOPS_2:78;
then FinMeetCl BB c= FinMeetCl the topology of T by CANTOR_1:16;
then A4: FinMeetCl BB c= the topology of T by A1, CANTOR_1:5;
consider A being Basis of T such that
A5: A c= FinMeetCl BB by A3, CANTOR_1:def 5;
A6: the topology of T c= UniCl A by CANTOR_1:def 2;
UniCl A c= UniCl (FinMeetCl BB) by A5, CANTOR_1:9;
then the topology of T c= UniCl (FinMeetCl BB) by A6, XBOOLE_1:1;
hence FinMeetCl BB is Basis of T by A4, CANTOR_1:def 2, TOPS_2:78; :: thesis: verum

end;

assume A7: FinMeetCl BB is Basis of T ; :: thesis: BB is prebasis of T
A8: BB c= FinMeetCl BB by CANTOR_1:4;
FinMeetCl BB c= the topology of T by A7, TOPS_2:78;
then BB c= the topology of T by A8, XBOOLE_1:1;
hence BB is prebasis of T by A7, CANTOR_1:def 5, TOPS_2:78; :: thesis: verum