let s be rectangular FinSequence of (TOP-REAL 2); :: thesis: ( s /. 2 = N-max (L~ s) & s /. 2 = E-max (L~ s) )
consider D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) such that
A1: s = SpStSeq D by Def2;
A2: s /. 2 = NE-corner D by A1, Th36;
hence s /. 2 = N-max (L~ s) by A1, Th77; :: thesis: s /. 2 = E-max (L~ s)
thus s /. 2 = E-max (L~ s) by A1, A2, Th79; :: thesis: verum