theorem :: SPRECT_1:83

for s being rectangular FinSequence of (TOP-REAL 2) holds
( s /. 1 = N-min (L~ s) & s /. 1 = W-max (L~ s) )