let z1, z2 be Quaternion; :: thesis: ( |.z1.| - |.z2.| <> 0 implies ((|.z1.| ^2) + (|.z2.| ^2)) - ((2 * |.z1.|) * |.z2.|) > 0 )
assume |.z1.| - |.z2.| <> 0 ; :: thesis: ((|.z1.| ^2) + (|.z2.| ^2)) - ((2 * |.z1.|) * |.z2.|) > 0
then (|.z1.| - |.z2.|) ^2 > 0 by SQUARE_1:12;
hence ((|.z1.| ^2) + (|.z2.| ^2)) - ((2 * |.z1.|) * |.z2.|) > 0 ; :: thesis: verum