let X be non empty set ; :: thesis: for B being filter_base of X holds B is basis of <.B.)
let B be filter_base of X; :: thesis: B is basis of <.B.)
reconsider B2 = <.B.) as Filter of X ;
B is non empty filter_basis Subset of B2

proof

B is non empty Subset of B2

proof

B c= B2 by def3;
hence B is non empty Subset of B2 ; :: thesis: verum

end;

then reconsider B3 = B as non empty Subset of B2 ;
B3 is filter_basis by def3;
hence B is non empty filter_basis Subset of B2 ; :: thesis: verum

end;

hence B is basis of <.B.) ; :: thesis: verum