consider D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2);
take SpStSeq D ; :: thesis: SpStSeq D is rectangular
take D ; :: according to SPRECT_1:def 2 :: thesis: SpStSeq D = SpStSeq D
thus SpStSeq D = SpStSeq D ; :: thesis: verum