let S be Subset of (TOP-REAL 2); :: thesis: (SpStSeq S) /. 3 = SE-corner S
3 in dom <*(NW-corner S),(NE-corner S),(SE-corner S)*> by FINSEQ_1:81;
hence (SpStSeq S) /. 3 = <*(NW-corner S),(NE-corner S),(SE-corner S)*> /. 3 by FINSEQ_4:68
.= SE-corner S by FINSEQ_4:18 ;
:: thesis: verum