len <*x,y,z*> = 3 by FINSEQ_1:45;
hence not <*x,y,z*> is trivial by NAT_D:60; :: thesis: verum