let Gi be non trivial finite Subset of REAL ; :: thesis: ex li, ri being Real st
( li in Gi & ri in Gi & ri < li & ( for xi being Real st xi in Gi holds
( not xi < ri & not li < xi ) ) )
consider li being Real such that
A1: ( li in Gi & ( for xi being Real st xi in Gi holds
li >= xi ) ) by Th12;
consider ri being Real such that
A2: ( ri in Gi & ( for xi being Real st xi in Gi holds
ri <= xi ) ) by Th13;
take li ; :: thesis: ex ri being Real st
( li in Gi & ri in Gi & ri < li & ( for xi being Real st xi in Gi holds
( not xi < ri & not li < xi ) ) )
take ri ; :: thesis: ( li in Gi & ri in Gi & ri < li & ( for xi being Real st xi in Gi holds
( not xi < ri & not li < xi ) ) )
A3: ri <= li by A1, A2;

now

assume A4: li = ri ; :: thesis: contradiction
consider x1, x2 being set such that
A5: ( x1 in Gi & x2 in Gi & x1 <> x2 ) by ZFMISC_1:def 10;
reconsider x1 = x1, x2 = x2 as Real by A5;
( ri <= x1 & x1 <= li & ri <= x2 & x2 <= li ) by A1, A2, A5;
then ( x1 = li & x2 = li ) by A4, XXREAL_0:1;
hence contradiction by A5; :: thesis: verum

end;

hence ( li in Gi & ri in Gi & ri < li & ( for xi being Real st xi in Gi holds
( not xi < ri & not li < xi ) ) ) by A1, A2, A3, XXREAL_0:1; :: thesis: verum