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 Th66
.= NW-corner C by Th68 ; :: thesis: verum