theorem Th12: :: XXREAL_1:12

for x being set
for p, q being ExtReal st x in ].p,q.] holds
( x in [.p,q.] & x <> p )