let X be non empty set ; :: thesis: for F being Filter of X holds F is basis of F
let F be Filter of X; :: thesis: F is basis of F
thus F is non empty filter_basis Subset of F :: thesis: verum
proof
( not F is empty & F c= F ) ;
then reconsider F0 = F as non empty Subset of F ;
F0 is filter_basis ;
hence F is non empty filter_basis Subset of F ; :: thesis: verum
end;