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