consider X being non empty compact non horizontal non vertical Subset of (TOP-REAL 2);
take SpStSeq X ; :: thesis: SpStSeq X is clockwise_oriented
thus SpStSeq X is clockwise_oriented ; :: thesis: verum