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: ( T is empty implies the topology of T = bool the carrier of T ) by ZFMISC_1:1, Th8;
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 TOPS_2:64;
then FinMeetCl BB c= FinMeetCl the topology of T by CANTOR_1:14;
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 4;
A5: the topology of T c= UniCl A by CANTOR_1:def 2;
UniCl A c= UniCl (FinMeetCl BB) by A4, CANTOR_1:9;
then the topology of T c= UniCl (FinMeetCl BB) by A5;
hence FinMeetCl BB is Basis of T by A3, CANTOR_1:def 2, TOPS_2:64; :: thesis: verum
end;
assume A6: FinMeetCl BB is Basis of T ; :: thesis: BB is prebasis of T
A7: BB c= FinMeetCl BB by CANTOR_1:4;
FinMeetCl BB c= the topology of T by A6, TOPS_2:64;
then BB c= the topology of T by A7;
hence BB is prebasis of T by A6, CANTOR_1:def 4, TOPS_2:64; :: thesis: verum