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