let S be Subset of (TOP-REAL 2); :: thesis: (SpStSeq S) /. 1 = NW-corner S
1 in dom <*(NW-corner S),(NE-corner S),(SE-corner S)*> by TOPREAL3:6;
hence (SpStSeq S) /. 1 = <*(NW-corner S),(NE-corner S),(SE-corner S)*> /. 1 by FINSEQ_4:83
.= NW-corner S by FINSEQ_4:27 ;
:: thesis: verum