theorem Th15: :: XXREAL_1:15

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