consider A, B being set such that

A3: ( A in F & B in F & ( for Y being set holds

( Y in F iff ( A c= Y & Y c= B ) ) ) ) by Def8;

A4: for Z1 being set st Z1 in F holds

Z1 c= B by A3;

A5: A c= union F by A3, ZFMISC_1:74;

union F c= B by A4, ZFMISC_1:76;

hence max F is Element of F by A3, A5; :: thesis: verum

A3: ( A in F & B in F & ( for Y being set holds

( Y in F iff ( A c= Y & Y c= B ) ) ) ) by Def8;

A4: for Z1 being set st Z1 in F holds

Z1 c= B by A3;

A5: A c= union F by A3, ZFMISC_1:74;

union F c= B by A4, ZFMISC_1:76;

hence max F is Element of F by A3, A5; :: thesis: verum