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

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