let X be non empty set ; :: thesis: {X} is Filter of X
( {X} is non empty Subset-Family of X & not {} in {X} & ( for Y1, Y2 being Subset of X holds
( ( Y1 in {X} & Y2 in {X} implies Y1 /\ Y2 in {X} ) & ( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} ) ) ) ) by Th2;
hence {X} is Filter of X by Def1; :: thesis: verum