let A be non empty closed_interval Subset of REAL; :: thesis: for x being Real holds
( x in A iff ( lower_bound A <= x & x <= upper_bound A ) )
let x be Real; :: thesis: ( x in A iff ( lower_bound A <= x & x <= upper_bound A ) )

hereby :: thesis: ( lower_bound A <= x & x <= upper_bound A implies x in A )

assume x in A ; :: thesis: ( lower_bound A <= x & x <= upper_bound A )
then x in [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then x in { a where a is Real : ( lower_bound A <= a & a <= upper_bound A ) } by RCOMP_1:def 1;
then ex a being Real st
( a = x & lower_bound A <= a & a <= upper_bound A ) ;
hence ( lower_bound A <= x & x <= upper_bound A ) ; :: thesis: verum

end;

assume A1: ( lower_bound A <= x & x <= upper_bound A ) ; :: thesis: x in A
x in { a where a is Real : ( lower_bound A <= a & a <= upper_bound A ) } by A1;
then x in [.(lower_bound A),(upper_bound A).] by RCOMP_1:def 1;
hence x in A by INTEGRA1:4; :: thesis: verum