let p, q be Element of REAL 3; :: thesis: |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)|
|((p - q),(p - q))| = ((|(p,p)| - |(p,q)|) - |(q,p)|) + |(q,q)| by Th78;
hence |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)| ; :: thesis: verum