thus
not REAL is bounded_below
:: thesis: not REAL is bounded_above

consider s being Real such that

A4: r < s by XREAL_1:1;

s in REAL by XREAL_0:def 1;

hence contradiction by A3, A4, Def1; :: thesis: verum

proof

given r being Real such that A3:
r is UpperBound of REAL
; :: according to XXREAL_2:def 10 :: thesis: contradiction
given r being Real such that A1:
r is LowerBound of REAL
; :: according to XXREAL_2:def 9 :: thesis: contradiction

consider s being Real such that

A2: s < r by XREAL_1:2;

s in REAL by XREAL_0:def 1;

hence contradiction by A1, A2, Def2; :: thesis: verum

end;consider s being Real such that

A2: s < r by XREAL_1:2;

s in REAL by XREAL_0:def 1;

hence contradiction by A1, A2, Def2; :: thesis: verum

consider s being Real such that

A4: r < s by XREAL_1:1;

s in REAL by XREAL_0:def 1;

hence contradiction by A3, A4, Def1; :: thesis: verum