theorem Th2: :: CURVE:2

for a, b being Real
for Z being open Subset of REAL st a < b & [.a,b.] c= Z holds
ex a1, b1 being Real st
( a1 < a & b < b1 & a1 < b1 & [.a1,b1.] c= Z & [.a,b.] c= ].a1,b1.[ )