theorem Th1: :: TOPGEN_6:1

for x, a, b being Real st x in ].a,b.[ holds
ex p, r being Rational st
( x in ].p,r.[ & ].p,r.[ c= ].a,b.[ )