theorem :: SPRECT_1:85

for s being rectangular FinSequence of (TOP-REAL 2) holds
( s /. 3 = S-max (L~ s) & s /. 3 = E-min (L~ s) )