let r, s be ExtReal; :: 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 ExtReal; :: according to MEMBERED:def 8 :: thesis: ( not t in [.r,s.] or t in {r} )
assume A2: t in [.r,s.] ; :: thesis: t in {r}
then A3: t <= s by Th1;
A4: r <= t by A2, Th1;
t <= r by A1, A3, XXREAL_0:2;
then r = t by A4, XXREAL_0:1;
hence t in {r} by TARSKI:def 1; :: thesis: verum

end;

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