let X be ext-real-membered set ; :: thesis: ( X is real-bounded implies X is real-membered )
assume A1: X is real-bounded ; :: thesis: X is real-membered
let x be object ; :: according to MEMBERED:def 3 :: thesis: ( not x in X or x is real )
assume A2: x in X ; :: thesis: x is real
then reconsider X = X as ext-real-membered non empty set ;
consider s being Real such that
A3: s is UpperBound of X by A1, Def10;
reconsider x = x as ExtReal by A2;
A4: s in REAL by XREAL_0:def 1;
A5: x <= s by A2, A3, Def1;
consider r being Real such that
A6: r is LowerBound of X by A1, Def9;
A7: r in REAL by XREAL_0:def 1;
r <= x by A2, A6, Def2;
then x in REAL by A5, A7, A4, XXREAL_0:45;
hence x is real ; :: thesis: verum