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