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

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

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

end;

assume B1: for Y being set st Y in F holds
Y c= G ; :: thesis: G = max F
B2: G c= max F by A, ZFMISC_1:92;
max F c= G by B1;
hence G = max F by B2, XBOOLE_0:def 10; :: thesis: verum