for a, b being Real
for A being non empty closed_interval Subset of REAL st A = [.a,b.] holds
( upper_bound A = b & lower_bound A = a )