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