theorem :: SPRECT_1:84

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