theorem Th3: :: INTEGR26:3

for a, b being Real
for I being Interval st a in I & b in I holds
[.a,b.] c= I