let r be Real; :: thesis: for s being ExtReal
for A being Subset of REAL st A c= ].s,r.[ holds
A is bounded_above
let s be ExtReal; :: thesis: for A being Subset of REAL st A c= ].s,r.[ holds
A is bounded_above
let A be Subset of REAL; :: thesis: ( A c= ].s,r.[ implies A is bounded_above )
assume A1: A c= ].s,r.[ ; :: thesis: A is bounded_above
].s,r.[ c= ].s,r.] by XXREAL_1:21;
then A c= ].s,r.] by A1;
hence A is bounded_above by XXREAL_2:43; :: thesis: verum