let X be non empty set ; :: thesis: {X} is Filter of X
A1: 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;
( {X} is non empty Subset-Family of X & not {} in {X} ) by Th2;
hence {X} is Filter of X by A1, Def1; :: thesis: verum