theorem Th3: :: INTEGRA1:5

for A being non empty closed_interval Subset of REAL
for a1, a2, b1, b2 being Real st A = [.a1,b1.] & A = [.a2,b2.] holds
( a1 = a2 & b1 = b2 )