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;
now :: thesis: ( s1 <= r & r <= s2 implies r in [.s1,s2.] )
assume ( 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;
hence ( r in [.s1,s2.] iff ( s1 <= r & r <= s2 ) ) by A1; :: thesis: verum