let X be compact Subset of R^1; :: thesis: for X9 being Subset of REAL
for x being Real st x in X9 & X9 = X holds
( lower_bound X9 <= x & x <= upper_bound X9 )
let X9 be Subset of REAL; :: thesis: for x being Real st x in X9 & X9 = X holds
( lower_bound X9 <= x & x <= upper_bound X9 )
let x be Real; :: thesis: ( x in X9 & X9 = X implies ( lower_bound X9 <= x & x <= upper_bound X9 ) )
assume that
A1: x in X9 and
A2: X9 = X ; :: thesis: ( lower_bound X9 <= x & x <= upper_bound X9 )
( X9 is bounded_above & X9 is bounded_below ) by A2, Th72;
hence ( lower_bound X9 <= x & x <= upper_bound X9 ) by A1, SEQ_4:def 1, SEQ_4:def 2; :: thesis: verum