set F = the Filter of X;
take dual the Filter of X ; :: thesis: ( not X in dual the Filter of X & ( for Y1, Y2 being Subset of X holds
( ( Y1 in dual the Filter of X & Y2 in dual the Filter of X implies Y1 \/ Y2 in dual the Filter of X ) & ( Y1 in dual the Filter of X & Y2 c= Y1 implies Y2 in dual the Filter of X ) ) ) )
for Y1 being Subset of X holds
( Y1 in dual the Filter of X iff Y1 ` in the Filter of X ) by SETFAM_1:def 7;
hence ( not X in dual the Filter of X & ( for Y1, Y2 being Subset of X holds
( ( Y1 in dual the Filter of X & Y2 in dual the Filter of X implies Y1 \/ Y2 in dual the Filter of X ) & ( Y1 in dual the Filter of X & Y2 c= Y1 implies Y2 in dual the Filter of X ) ) ) ) by Th7; :: thesis: verum