let C be non empty compact Subset of ; :: 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