let SF be non empty Subset-Family of [:X,X:]; :: thesis: ( SF is cap-closed implies SF is quasi_basis )
assume A1: SF is cap-closed ; :: thesis: SF is quasi_basis
now :: thesis: for b1, b2 being Element of SF ex b being Element of SF st b c= b1 /\ b2
let b1, b2 be Element of SF; :: thesis: ex b being Element of SF st b c= b1 /\ b2
b1 /\ b2 in SF by A1, FINSUB_1:def 2;
hence ex b being Element of SF st b c= b1 /\ b2 ; :: thesis: verum
end;
hence SF is quasi_basis ; :: thesis: verum