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;

( not xi < ri & not li < xi ) ) ) by A1, A2, A3, A4, A5, XXREAL_0:1; :: thesis: verum

( 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

hence
( li in Gi & ri in Gi & ri < li & ( for xi being Real st xi in Gi holds 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;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

( not xi < ri & not li < xi ) ) ) by A1, A2, A3, A4, A5, XXREAL_0:1; :: thesis: verum