take S = {X}; :: thesis: ( S is non empty Subset-Family of X & S is quasi_basis )
thus S is non empty Subset-Family of X by CARD_FIL:2; :: thesis: S is quasi_basis
reconsider S1 = S as Subset-Family of X by CARD_FIL:2;

now :: thesis: for b1, b2 being Element of S1 ex b being Element of S1 st b c= b1 /\ b2

let b1, b2 be Element of S1; :: thesis: ex b being Element of S1 st b c= b1 /\ b2
set b = b1 /\ b2;
( b1 = X & b2 = X ) by TARSKI:def 1;
hence ex b being Element of S1 st b c= b1 /\ b2 ; :: thesis: verum

end;

then S1 is quasi_basis ;
hence S is quasi_basis ; :: thesis: verum