let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is rectangular implies not f is constant )
assume ex D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) st f = SpStSeq D ; :: according to SPRECT_1:def 2 :: thesis: not f is constant
hence not f is constant ; :: thesis: verum