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