let X be set ; :: thesis: for F being non empty ordered Subset-Family of
for G being set st G in F holds
( G = min F iff for Y being set st Y in F holds
G c= Y )
let F be non empty ordered Subset-Family of ; :: thesis: for G being set st G in F holds
( G = min F iff for Y being set st Y in F holds
G c= Y )
let G be set ; :: thesis: ( G in F implies ( G = min F iff for Y being set st Y in F holds
G c= Y ) )
assume A: G in F ; :: thesis: ( G = min F iff for Y being set st Y in F holds
G c= Y )

hereby :: thesis: ( ( for Y being set st Y in F holds
G c= Y ) implies G = min F )

assume A1: G = min F ; :: thesis: for Y being set st Y in F holds
G c= Y
let Y be set ; :: thesis: ( Y in F implies G c= Y )
assume Y in F ; :: thesis: G c= Y
hence G c= Y by A1, SETFAM_1:4; :: thesis: verum

end;

assume for Y being set st Y in F holds
G c= Y ; :: thesis: G = min F
then B2: G c= min F ;
min F c= G by A, SETFAM_1:4;
hence G = min F by B2, XBOOLE_0:def 10; :: thesis: verum