let s be rectangular FinSequence of (TOP-REAL 2); :: thesis: ( s /. 4 = S-min (L~ s) & s /. 4 = W-min (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 /. 4 = SW-corner D by A1, Th38;
hence s /. 4 = S-min (L~ s) by A1, Th80; :: thesis: s /. 4 = W-min (L~ s)
thus s /. 4 = W-min (L~ s) by A1, A2, Th74; :: thesis: verum