A1: Rea 0q = 0 by Lm7, Th23;
A2: Im1 0q = 0 by Lm7, Th23;
Im2 0q = 0 by Lm7, Th23;
hence |.0q.| = 0 by A1, A2, Lm7, Th23, SQUARE_1:17; :: thesis: verum