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