theorem :: SPRECT_1:82

for s being rectangular FinSequence of (TOP-REAL 2) holds len s = 5