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