let x, y, z be object ; :: thesis: ( 1 in dom <*x,y,z*> & 2 in dom <*x,y,z*> & 3 in dom <*x,y,z*> )
len <*x,y,z*> = 3 by Th45;
then dom <*x,y,z*> = Seg 3 by Def3;
hence ( 1 in dom <*x,y,z*> & 2 in dom <*x,y,z*> & 3 in dom <*x,y,z*> ) ; :: thesis: verum