let u, x, y, z be set ; :: thesis: <*u*> <> <*x,y,z*>
len <*u*> = 1 by FINSEQ_1:57;
hence <*u*> <> <*x,y,z*> by FINSEQ_1:62; :: thesis: verum