for Y1 being Subset of X holds

( Y1 in dual F iff Y1 ` in F ) by SETFAM_1:def 7;

then ( 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;

hence dual F is Ideal of X by Def2; :: thesis: verum

( Y1 in dual F iff Y1 ` in F ) by SETFAM_1:def 7;

then ( 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;

hence dual F is Ideal of X by Def2; :: thesis: verum