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