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 A' = A as Subset-Family of TopStruct(# X,(UniCl (FinMeetCl A)) #) ;
A' is prebasis of TopStruct(# X,(UniCl (FinMeetCl A)) #)

proof

( A' c= FinMeetCl A & FinMeetCl A c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ) by Th1, Th4;
hence A' c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) by XBOOLE_1:1; :: according to CANTOR_1:def 5 :: thesis: ex F being Basis of TopStruct(# X,(UniCl (FinMeetCl A)) #) st F c= FinMeetCl A'
reconsider B = FinMeetCl A' as Basis of TopStruct(# X,(UniCl (FinMeetCl A)) #) by Th18;
take B ; :: thesis: B c= FinMeetCl A'
thus B c= FinMeetCl A' ; :: thesis: verum

end;

hence A is prebasis of TopStruct(# X,(UniCl (FinMeetCl A)) #) ; :: thesis: verum