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