let Gi be non trivial finite Subset of REAL; 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
; 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
; ( 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 not li = riassume A6:
li = ri
;
contradictionconsider 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;
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; verum