theorem :: QUATERNI:71

|.<k>.| = 1 by Th24, SQUARE_1:18;