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