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

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