let s, r be ext-real number ; :: thesis: ( s <= r implies ( [.r,s.] c= {r} & [.r,s.] c= {s} ) )
assume A1: s <= r ; :: thesis: ( [.r,s.] c= {r} & [.r,s.] c= {s} )
thus [.r,s.] c= {r} :: thesis: [.r,s.] c= {s}

proof

let t be ext-real number ; :: according to MEMBERED:def 8 :: thesis: ( not t in [.r,s.] or t in {r} )
assume t in [.r,s.] ; :: thesis: t in {r}
then ( r <= t & t <= s ) by Th1;
then ( r <= t & t <= r ) by A1, XXREAL_0:2;
then r = t by XXREAL_0:1;
hence t in {r} by TARSKI:def 1; :: thesis: verum

end;

let t be ext-real number ; :: according to MEMBERED:def 8 :: thesis: ( not t in [.r,s.] or t in {s} )
assume t in [.r,s.] ; :: thesis: t in {s}
then ( r <= t & t <= s ) by Th1;
then ( s <= t & t <= s ) by A1, XXREAL_0:2;
then s = t by XXREAL_0:1;
hence t in {s} by TARSKI:def 1; :: thesis: verum