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

proof

given r being real number such that G: r is LowerBound of REAL ; :: according to XXREAL_2:def 9 :: thesis: contradiction
consider s being real number such that
W: s < r by XREAL_1:4;
s in REAL by XREAL_0:def 1;
hence contradiction by W, G, Def2; :: thesis: verum

end;

given r being real number such that G: r is UpperBound of REAL ; :: according to XXREAL_2:def 10 :: thesis: contradiction
consider s being real number such that
W: r < s by XREAL_1:3;
s in REAL by XREAL_0:def 1;
hence contradiction by W, G, Def1; :: thesis: verum