let a, b, c, x be Real; :: 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.[
( x <= a or x >= b ) by A2, XXREAL_1:4;
then A4: x > b by A1, A3, XXREAL_0:1, XXREAL_1:4;
x < c by A1, XXREAL_1:4;
hence x in ].b,c.[ by A4, XXREAL_1:4; :: thesis: verum