consider li, ri being Real such that
A1: li in Gi and
A2: ri in Gi and
A3: li < ri and
A4: for xi being Real st xi in Gi & li < xi holds
not xi < ri by Th11;
reconsider ri = ri, li = li as Element of REAL by XREAL_0:def 1;
take [li,ri] ; :: thesis: ex li, ri being Real st
( [li,ri] = [li,ri] & li in Gi & ri in Gi & ( ( li < ri & ( for xi being Real st xi in Gi & li < xi holds
not xi < ri ) ) or ( ri < li & ( for xi being Real st xi in Gi holds
( not li < xi & not xi < ri ) ) ) ) )
take li ; :: thesis: ex ri being Real st
( [li,ri] = [li,ri] & li in Gi & ri in Gi & ( ( li < ri & ( for xi being Real st xi in Gi & li < xi holds
not xi < ri ) ) or ( ri < li & ( for xi being Real st xi in Gi holds
( not li < xi & not xi < ri ) ) ) ) )
take ri ; :: thesis: ( [li,ri] = [li,ri] & li in Gi & ri in Gi & ( ( li < ri & ( for xi being Real st xi in Gi & li < xi holds
not xi < ri ) ) or ( ri < li & ( for xi being Real st xi in Gi holds
( not li < xi & not xi < ri ) ) ) ) )
thus ( [li,ri] = [li,ri] & li in Gi & ri in Gi & ( ( li < ri & ( for xi being Real st xi in Gi & li < xi holds
not xi < ri ) ) or ( ri < li & ( for xi being Real st xi in Gi holds
( not li < xi & not xi < ri ) ) ) ) ) by A1, A2, A3, A4; :: thesis: verum