let T be non empty TopSpace; :: thesis: for B being Subset-Family of T st UniCl B is prebasis of T holds
B is prebasis of T
let B be Subset-Family of T; :: thesis: ( UniCl B is prebasis of T implies B is prebasis of T )
assume UniCl B is prebasis of T ; :: thesis: B is prebasis of T
then FinMeetCl (UniCl B) is Basis of T by Th23;
then UniCl (FinMeetCl (UniCl B)) = the topology of T by Th22;
then UniCl (FinMeetCl B) = the topology of T by Th21;
then FinMeetCl B is Basis of T by Th22;
hence B is prebasis of T by Th23; :: thesis: verum