theorem Th31: :: TOPREALA:31

for a, b, r, s being Real st a <= b & r <= s holds
|[a,r]| in closed_inside_of_rectangle (a,b,r,s)