let X be non empty set ; :: thesis: for F being Filter of X
for B being basis of F holds B is filter_base of X
let F be Filter of X; :: thesis: for B being basis of F holds B is filter_base of X
let B be basis of F; :: thesis: B is filter_base of X
for b1, b2 being Element of B ex b being Element of B st b c= b1 /\ b2
proof
let b1, b2 be Element of B; :: thesis: ex b being Element of B st b c= b1 /\ b2
b1 /\ b2 in F by CARD_FIL:def 1;
then consider b0 being Element of B such that
A1: b0 c= b1 /\ b2 by def2;
thus ex b being Element of B st b c= b1 /\ b2 by A1; :: thesis: verum
end;
then A2: # B is quasi_basis ;
B is with_non-empty_elements by CARD_FIL:def 1;
hence B is filter_base of X by A2; :: thesis: verum