let X be non empty set ; :: thesis:
let FB be filter_base of X; :: thesis:
let F be Filter of X; :: thesis:
assume A1: FB c= F ; :: thesis:

let x be object ; :: thesis:
assume A2: x in <.FB.) ; :: thesis:
then reconsider x1 = x as Subset of X ;
consider b being Element of FB such that
A4: b c= x1 by A2, def3;
A5: b in F by A1;
reconsider x2 = x1 as Subset of X ;
consider c being Element of F such that
A6: c c= x2 by A4, A5;
thus x in F by A6, CARD_FIL:def 1; :: thesis:

end;