let p, q, r, s be ExtReal; :: thesis: ( r < s & ].r,s.[ c= [.p,q.] implies [.r,s.] c= [.p,q.] )
assume that
A1: r < s and
A2: ].r,s.[ c= [.p,q.] ; :: thesis: [.r,s.] c= [.p,q.]
let t be ExtReal; :: according to MEMBERED:def 8 :: thesis: ( not t in [.r,s.] or t in [.p,q.] )
assume A3: t in [.r,s.] ; :: thesis: t in [.p,q.]

per cases ( t in ].r,s.[ or t = r or t = s ) by A3, Th5;

suppose t in ].r,s.[ ; :: thesis: t in [.p,q.]

hence t in [.p,q.] by A2; :: thesis: verum

end;

suppose A4: t = r ; :: thesis: t in [.p,q.]

then A5: p <= t by A1, A2, Th51;
s <= q by A1, A2, Th51;
then t <= q by A1, A4, XXREAL_0:2;
hence t in [.p,q.] by A5, Th1; :: thesis: verum

end;

suppose A6: t = s ; :: thesis: t in [.p,q.]

A7: s <= q by A1, A2, Th51;
p <= r by A1, A2, Th51;
then p <= t by A1, A6, XXREAL_0:2;
hence t in [.p,q.] by A6, A7, Th1; :: thesis: verum

end;

end;