let x be ExtReal; :: according to XXREAL_2:def 12 :: thesis: for s being ExtReal st x in ].r,s.[ & s in ].r,s.[ holds
[.x,s.] c= ].r,s.[
let y be ExtReal; :: thesis: ( x in ].r,s.[ & y in ].r,s.[ implies [.x,y.] c= ].r,s.[ )
assume x in ].r,s.[ ; :: thesis: ( not y in ].r,s.[ or [.x,y.] c= ].r,s.[ )
then A13: r < x by XXREAL_1:4;
assume y in ].r,s.[ ; :: thesis: [.x,y.] c= ].r,s.[
then A14: y < s by XXREAL_1:4;
let z be ExtReal; :: according to MEMBERED:def 8 :: thesis: ( not z in [.x,y.] or z in ].r,s.[ )
assume A15: z in [.x,y.] ; :: thesis: z in ].r,s.[
then x <= z by XXREAL_1:1;
then A16: r < z by A13, XXREAL_0:2;
z <= y by A15, XXREAL_1:1;
then z < s by A14, XXREAL_0:2;
hence z in ].r,s.[ by A16, XXREAL_1:4; :: thesis: verum