for I being non empty closed_interval Subset of REAL
for c being Real st c in I holds
( [.(lower_bound I),c.] is non empty closed_interval Subset of REAL & [.c,(upper_bound I).] is non empty closed_interval Subset of REAL & upper_bound [.(lower_bound I),c.] = lower_bound [.c,(upper_bound I).] )