A1: Rea 1q = 1 by Lm11, Th23;
A2: Im1 1q = 0 by Lm11, Th23;
Im2 1q = 0 by Lm11, Th23;
hence |.1q.| = 1 by A1, A2, Lm11, Th23, SQUARE_1:18; :: thesis: verum