let X be non empty set ; :: thesis: for F being Filter of X
for B being Subset-Family of X st F = <.B.] holds
B is basis of F
let F be Filter of X; :: thesis: for B being Subset-Family of X st F = <.B.] holds
B is basis of F
let B be Subset-Family of X; :: thesis: ( F = <.B.] implies B is basis of F )
assume A1: F = <.B.] ; :: thesis: B is basis of F
then A2: B c= F by def3;
not B is empty
proof
assume A3I1: B is empty ; :: thesis: contradiction
A4I2A: {} c= X ;
{} is Element of B by A3I1, SUBSET_1:def 1;
then {} in <.B.] by A4I2A, def3;
hence contradiction by A1, CARD_FIL:def 1; :: thesis: verum
end;
then reconsider B1 = B as non empty Subset of F by A2;
B1 is filter_basis by A1, def3;
hence B is basis of F ; :: thesis: verum