thus not REAL is bounded_below :: thesis: not REAL is bounded_above
proof
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;
given r being Real such that A3: r is UpperBound of REAL ; :: according to XXREAL_2:def 10 :: thesis: contradiction
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