set S = {X};
reconsider S1 = {X} 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 ;
then reconsider S2 = S1 as non empty quasi_basis Subset-Family of X ;
S2 is with_non-empty_elements ;
hence ex b₁ being non empty quasi_basis Subset-Family of X st b₁ is with_non-empty_elements ; :: thesis: verum