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 ) )

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

( 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 A1:
( lower_bound A <= x & x <= upper_bound A )
; :: thesis: x in Aassume
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;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

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