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 Th61
.= NE-corner C by Th60 ; :: thesis: verum