let A, E, F be Point of (TOP-REAL 2); :: thesis: |.(F - E).| ^2 = ((|.(A - E).| ^2) + (|.(A - F).| ^2)) - (((2 * |.(A - E).|) * |.(A - F).|) * (cos (angle (E,A,F))))
|.(F - E).| ^2 = ((|.(E - A).| ^2) + (|.(F - A).| ^2)) - (((2 * |.(E - A).|) * |.(F - A).|) * (cos (angle (E,A,F)))) by EUCLID_6:7
.= ((|.(A - E).| ^2) + (|.(F - A).| ^2)) - (((2 * |.(E - A).|) * |.(F - A).|) * (cos (angle (E,A,F)))) by EUCLID_6:43
.= ((|.(A - E).| ^2) + (|.(A - F).| ^2)) - (((2 * |.(E - A).|) * |.(F - A).|) * (cos (angle (E,A,F)))) by EUCLID_6:43
.= ((|.(A - E).| ^2) + (|.(A - F).| ^2)) - (((2 * |.(A - E).|) * |.(F - A).|) * (cos (angle (E,A,F)))) by EUCLID_6:43
.= ((|.(A - E).| ^2) + (|.(A - F).| ^2)) - (((2 * |.(A - E).|) * |.(A - F).|) * (cos (angle (E,A,F)))) by EUCLID_6:43 ;
hence |.(F - E).| ^2 = ((|.(A - E).| ^2) + (|.(A - F).| ^2)) - (((2 * |.(A - E).|) * |.(A - F).|) * (cos (angle (E,A,F)))) ; :: thesis: verum