let r, s be ExtReal; ( r < s implies ].r,s.] = ].r,s.[ \/ {s} )
assume A1:
r < s
; ].r,s.] = ].r,s.[ \/ {s}
let t be ExtReal; MEMBERED:def 14 ( ( not t in ].r,s.] or t in ].r,s.[ \/ {s} ) & ( not t in ].r,s.[ \/ {s} or t in ].r,s.] ) )
thus
( t in ].r,s.] implies t in ].r,s.[ \/ {s} )
( not t in ].r,s.[ \/ {s} or t in ].r,s.] )
assume
t in ].r,s.[ \/ {s}
; t in ].r,s.]
then
( t in ].r,s.[ or t in {s} )
by XBOOLE_0:def 3;
then
( t in ].r,s.[ or t = s )
by TARSKI:def 1;
hence
t in ].r,s.]
by A1, Th2, Th15; verum