let s be rectangular FinSequence of ; :: thesis: ( s /. 1 = N-min (L~ s) & s /. 1 = W-max (L~ s) )
consider D being non empty compact non horizontal non vertical Subset of such that
A1: s = SpStSeq D by Def2;
A2: s /. 1 = NW-corner D by A1, Th37;
hence s /. 1 = N-min (L~ s) by A1, Th84; :: thesis: s /. 1 = W-max (L~ s)
thus s /. 1 = W-max (L~ s) by A1, A2, Th83; :: thesis: verum