for X being non empty set
for F being set holds
( F is Filter of X iff ( F is non empty Subset-Family of X & not {} in F & ( for Y1, Y2 being Subset of X holds
( ( Y1 in F & Y2 in F implies Y1 /\ Y2 in F ) & ( Y1 in F & Y1 c= Y2 implies Y2 in F ) ) ) ) ) by Def1;