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