let x be ext-real number ; :: according to XXREAL_2:def 12 :: thesis: for s being ext-real number st x in ].r,s.] & s in ].r,s.] holds
[.x,s.] c= ].r,s.]
let y be ext-real number ; :: 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 A6: r < x by XXREAL_1:2;
assume y in ].r,s.] ; :: thesis: [.x,y.] c= ].r,s.]
then A7: y <= s by XXREAL_1:2;
let z be ext-real number ; :: according to MEMBERED:def 8 :: thesis: ( not z in [.x,y.] or z in ].r,s.] )
assume A8: z in [.x,y.] ; :: thesis: z in ].r,s.]
then x <= z by XXREAL_1:1;
then A9: r < z by A6, XXREAL_0:2;
z <= y by A8, XXREAL_1:1;
then z <= s by A7, XXREAL_0:2;
hence z in ].r,s.] by A9, XXREAL_1:2; :: thesis: verum