theorem Th6: :: COMPTRIG:6

for a, b, c, x being Real holds
( not x in ].a,c.[ or x in ].a,b.[ or x = b or x in ].b,c.[ )