let X be compact Subset of R^1 ; :: thesis: for X9 being Subset of REAL
for x being real number st x in X9 & X9 = X holds
( inf X9 <= x & x <= sup X9 )
let X9 be Subset of REAL ; :: thesis: for x being real number st x in X9 & X9 = X holds
( inf X9 <= x & x <= sup X9 )
let x be real number ; :: thesis: ( x in X9 & X9 = X implies ( inf X9 <= x & x <= sup X9 ) )
assume that
A1: x in X9 and
A2: X9 = X ; :: thesis: ( inf X9 <= x & x <= sup X9 )
( X9 is bounded_above & X9 is bounded_below ) by A2, Th107;
hence ( inf X9 <= x & x <= sup X9 ) by A1, SEQ_4:def 4, SEQ_4:def 5; :: thesis: verum