let a, b, c, x be real number ; :: thesis: ( not x in ].a,c.[ or x in ].a,b.[ or x = b or x in ].b,c.[ )
assume that
A1: x in ].a,c.[ and
A2: not x in ].a,b.[ and
A3: not x = b ; :: thesis: x in ].b,c.[
A4: ( a < x & x < c ) by A1, XXREAL_1:4;
( x <= a or x >= b ) by A2, XXREAL_1:4;
then x > b by A1, A3, XXREAL_0:1, XXREAL_1:4;
hence x in ].b,c.[ by A4, XXREAL_1:4; :: thesis: verum