theorem Th87: :: SPRECT_1:87
for r1, r2, s1, s2 being Real st r1 < r2 & s1 < s2 holds
[.r1,r2,s1,s2.] is Jordan