let s be rectangular FinSequence of (TOP-REAL 2); :: 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 (TOP-REAL 2) such that
A1: s = SpStSeq D by Def2;
A2: s /. 1 = NW-corner D by A1, Th35;
hence s /. 1 = N-min (L~ s) by A1, Th76; :: thesis: s /. 1 = W-max (L~ s)
thus s /. 1 = W-max (L~ s) by A1, A2, Th75; :: thesis: verum