let f be rectangular FinSequence of (TOP-REAL 2); :: thesis: LeftComp f <> RightComp f
LeftComp f misses RightComp f by Th88;
hence LeftComp f <> RightComp f ; :: thesis: verum