theorem :: AMI_8:2

for x1, x2, x3, x4 being object holds len <%x1,x2,x3,x4%> = 4 by Th1, CARD_1:52;