let x be ExtReal; XXREAL_2:def 12 for s being ExtReal st x in ].r,s.] & s in ].r,s.] holds
[.x,s.] c= ].r,s.]
let y be ExtReal; ( x in ].r,s.] & y in ].r,s.] implies [.x,y.] c= ].r,s.] )
assume
x in ].r,s.]
; ( not y in ].r,s.] or [.x,y.] c= ].r,s.] )
then A5:
r < x
by XXREAL_1:2;
assume
y in ].r,s.]
; [.x,y.] c= ].r,s.]
then A6:
y <= s
by XXREAL_1:2;
let z be ExtReal; MEMBERED:def 8 ( not z in [.x,y.] or z in ].r,s.] )
assume A7:
z in [.x,y.]
; z in ].r,s.]
then
x <= z
by XXREAL_1:1;
then A8:
r < z
by A5, XXREAL_0:2;
z <= y
by A7, XXREAL_1:1;
then
z <= s
by A6, XXREAL_0:2;
hence
z in ].r,s.]
by A8, XXREAL_1:2; verum