let X be non empty set ; :: thesis: for Y being Subset-Family of X holds Y is prebasis of TopStruct(# X,(UniCl (FinMeetCl Y)) #)
let A be Subset-Family of X; :: thesis: A is prebasis of TopStruct(# X,(UniCl (FinMeetCl A)) #)
set T = TopStruct(# X,(UniCl (FinMeetCl A)) #);
reconsider A9 = A as Subset-Family of TopStruct(# X,(UniCl (FinMeetCl A)) #) ;
now :: thesis: ( A9 is open & A9 is quasi_prebasis )
( A9 c= FinMeetCl A & FinMeetCl A c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ) by Th1, Th4;
then A9 c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ;
hence A9 is open by TOPS_2:64; :: thesis: A9 is quasi_prebasis
thus A9 is quasi_prebasis :: thesis: verum
proof
reconsider B = FinMeetCl A9 as Basis of TopStruct(# X,(UniCl (FinMeetCl A)) #) by Th16;
take B ; :: according to CANTOR_1:def 4 :: thesis: B c= FinMeetCl A9
thus B c= FinMeetCl A9 ; :: thesis: verum
end;
end;
hence A is prebasis of TopStruct(# X,(UniCl (FinMeetCl A)) #) ; :: thesis: verum