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 Element of REAL such that
A1: li in Gi and
A2: for xi being Real st xi in Gi holds
li >= xi by Th9;
consider ri being Element of REAL such that
A3: ri in Gi and
A4: for xi being Real st xi in Gi holds
ri <= xi by Th10;
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 ) ) )
A5: ri <= li by A2, A3;

now :: thesis: not li = ri

assume A6: li = ri ; :: thesis: contradiction
consider x1, x2 being object such that
A7: x1 in Gi and
A8: x2 in Gi and
A9: x1 <> x2 by ZFMISC_1:def 10;
reconsider x1 = x1, x2 = x2 as Element of REAL by A7, A8;
A10: ri <= x1 by A4, A7;
A11: x1 <= li by A2, A7;
A12: ri <= x2 by A4, A8;
A13: x2 <= li by A2, A8;
x1 = li by A6, A10, A11, XXREAL_0:1;
hence contradiction by A6, A9, A12, A13, XXREAL_0:1; :: 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, A4, A5, XXREAL_0:1; :: thesis: verum