let r, s1, s2 be Real; :: thesis: ( r in [.s1,s2.] iff ( s1 <= r & r <= s2 ) )

A1: now :: thesis: ( r in [.s1,s2.] implies ( s1 <= r & r <= s2 ) )

assume
r in [.s1,s2.]
; :: thesis: ( s1 <= r & r <= s2 )

then r in { r1 where r1 is Real : ( s1 <= r1 & r1 <= s2 ) } by RCOMP_1:def 1;

then ex r1 being Real st

( r1 = r & s1 <= r1 & r1 <= s2 ) ;

hence ( s1 <= r & r <= s2 ) ; :: thesis: verum

end;then r in { r1 where r1 is Real : ( s1 <= r1 & r1 <= s2 ) } by RCOMP_1:def 1;

then ex r1 being Real st

( r1 = r & s1 <= r1 & r1 <= s2 ) ;

hence ( s1 <= r & r <= s2 ) ; :: thesis: verum

now :: thesis: ( s1 <= r & r <= s2 implies r in [.s1,s2.] )

hence
( r in [.s1,s2.] iff ( s1 <= r & r <= s2 ) )
by A1; :: thesis: verumassume
( s1 <= r & r <= s2 )
; :: thesis: r in [.s1,s2.]

then r in { r1 where r1 is Real : ( s1 <= r1 & r1 <= s2 ) } ;

hence r in [.s1,s2.] by RCOMP_1:def 1; :: thesis: verum

end;then r in { r1 where r1 is Real : ( s1 <= r1 & r1 <= s2 ) } ;

hence r in [.s1,s2.] by RCOMP_1:def 1; :: thesis: verum