let x, y, z, w be Real; :: thesis: ( |.(x - y).| < |.(z - w).| implies (x - y) ^2 < (z - w) ^2 )
A2: |.(x - y).| ^2 = (x - y) ^2 by COMPLEX1:75;
assume |.(x - y).| < |.(z - w).| ; :: thesis: (x - y) ^2 < (z - w) ^2
then |.(x - y).| ^2 < |.(z - w).| ^2 by SQUARE_1:16;
hence (x - y) ^2 < (z - w) ^2 by COMPLEX1:75, A2; :: thesis: verum