let X be compact Subset of R^1 ; :: 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 A1: ( x in X' & X' = X ) ; :: thesis: ( inf X' <= x & x <= sup X' )
then ( X' is bounded_above & X' is bounded_below ) by Th107;
hence ( inf X' <= x & x <= sup X' ) by A1, SEQ_4:def 4, SEQ_4:def 5; :: thesis: verum