let X be ext-real-membered set ; :: thesis: ( X is bounded implies X is real-membered )
assume Z0: X is bounded ; :: thesis: X is real-membered
let x be set ; :: according to MEMBERED:def 3 :: thesis: ( not x in X or x is real )
assume Z: x in X ; :: thesis: x is real
then reconsider x = x as ext-real number ;
reconsider X = X as ext-real-membered non empty set by Z;
consider r being real number such that
W1: r is LowerBound of X by Def9, Z0;
consider s being real number such that
W2: s is UpperBound of X by Def10, Z0;
A: ( r <= x & x <= s ) by Z, W1, W2, Def1, Def2;
( r in REAL & s in REAL ) by XREAL_0:def 1;
then x in REAL by A, XXREAL_0:45;
hence x is real ; :: thesis: verum