theorem Th3: :: EUCLID11:4

for A, E, F being Point of (TOP-REAL 2) holds |.(F - E).| ^2 = ((|.(A - E).| ^2) + (|.(A - F).| ^2)) - (((2 * |.(A - E).|) * |.(A - F).|) * (cos (angle (E,A,F))))