let C be non empty compact Subset of (TOP-REAL 2); :: thesis: NW-corner (L~ (SpStSeq C)) = NW-corner C
thus NW-corner (L~ (SpStSeq C)) = |[(W-bound C),(N-bound (L~ (SpStSeq C)))]| by Th58
.= NW-corner C by Th60 ; :: thesis: verum