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

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