let s be rectangular FinSequence of (TOP-REAL 2); :: thesis: ( s /. 3 = S-max (L~ s) & s /. 3 = E-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 /. 3 = SE-corner D by A1, Th37;
hence s /. 3 = S-max (L~ s) by A1, Th81; :: thesis: s /. 3 = E-min (L~ s)
thus s /. 3 = E-min (L~ s) by A1, A2, Th78; :: thesis: verum