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