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 T is empty ; :: thesis: the topology of T = bool the carrier of T
then ( the topology of T = {{} } & the carrier of T = {} ) by Th8;
hence the topology of T = bool the carrier of T by 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 A2: BB is prebasis of T ; :: thesis: FinMeetCl BB is Basis of T
then BB c= the topology of T by CANTOR_1:def 5;
then FinMeetCl BB c= FinMeetCl the topology of T by CANTOR_1:16;
then A3: FinMeetCl BB c= the topology of T by A1, CANTOR_1:5;
consider A being Basis of T such that
A4: A c= FinMeetCl BB by A2, CANTOR_1:def 5;
( the topology of T c= UniCl A & UniCl A c= UniCl (FinMeetCl BB) ) by A4, CANTOR_1:9, CANTOR_1:def 2;
then the topology of T c= UniCl (FinMeetCl BB) by XBOOLE_1:1;
hence FinMeetCl BB is Basis of T by A3, CANTOR_1:def 2; :: thesis: verum

end;

assume A5: FinMeetCl BB is Basis of T ; :: thesis: BB is prebasis of T
then ( BB c= FinMeetCl BB & FinMeetCl BB c= the topology of T ) by CANTOR_1:4, CANTOR_1:def 2;
then BB c= the topology of T by XBOOLE_1:1;
hence BB is prebasis of T by A5, CANTOR_1:def 5; :: thesis: verum