let F be Basis of X; :: thesis: F is quasi_prebasis
take F ; :: according to CANTOR_1:def 5 :: thesis: F c= FinMeetCl F
thus F c= FinMeetCl F by Th4; :: thesis: verum