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