len <*x,y*> = 2 by FINSEQ_1:61;
hence not <*x,y*> is trivial by REALSET1:13; :: thesis: verum