consider A, B being set such that

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

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

for Z1 being set st Z1 in F holds

A c= Z1 by A1;

then A2: A c= meet F by SETFAM_1:5;

meet F c= B by A1, SETFAM_1:3;

hence min F is Element of F by A1, A2; :: thesis: verum

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

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

for Z1 being set st Z1 in F holds

A c= Z1 by A1;

then A2: A c= meet F by SETFAM_1:5;

meet F c= B by A1, SETFAM_1:3;

hence min F is Element of F by A1, A2; :: thesis: verum