let u, v, x, y, z be object ; :: thesis: <*u,v*> <> <*x,y,z*>
len <*u,v*> = 2 by FINSEQ_1:44;
hence <*u,v*> <> <*x,y,z*> by FINSEQ_1:45; :: thesis: verum