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