let X be Subset of I[01] ; :: thesis: for X' being Subset of REAL
for x being real number st x in X' & X' = X holds
( inf X' <= x & x <= sup X' )
let X' be Subset of REAL ; :: thesis: for x being real number st x in X' & X' = X holds
( inf X' <= x & x <= sup X' )
let x be real number ; :: thesis: ( x in X' & X' = X implies ( inf X' <= x & x <= sup X' ) )
assume that
A1: x in X' and
A2: X' = X ; :: thesis: ( inf X' <= x & x <= sup X' )
( X' is bounded_above & X' is bounded_below ) by A2, Th50;
hence ( inf X' <= x & x <= sup X' ) by A1, SEQ_4:def 4, SEQ_4:def 5; :: thesis: verum