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