let X be non empty set ; :: thesis: for Y being Subset-Family of holds Y is prebasis of TopStruct(# X,(UniCl (FinMeetCl Y)) #)
let A be Subset-Family of ; :: thesis: A is prebasis of TopStruct(# X,(UniCl (FinMeetCl A)) #)
set T = TopStruct(# X,(UniCl (FinMeetCl A)) #);
reconsider A' = A as Subset-Family of ;

now

( A' c= FinMeetCl A & FinMeetCl A c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ) by Th1, Th4;
then A' c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) by XBOOLE_1:1;
hence A' is open by TOPS_2:78; :: thesis: A' is quasi_prebasis
thus A' is quasi_prebasis :: thesis: verum

proof

reconsider B = FinMeetCl A' as Basis of TopStruct(# X,(UniCl (FinMeetCl A)) #) by Th18;
take B ; :: according to CANTOR_1:def 5 :: thesis: B c= FinMeetCl A'
thus B c= FinMeetCl A' ; :: thesis: verum

end;

end;

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