theorem Th7: :: EUCLID_6:7

for p1, p2, p3 being Point of (TOP-REAL 2)
for a, b, c being Real st a = |.(p1 - p2).| & b = |.(p3 - p2).| & c = |.(p3 - p1).| holds
c ^2 = ((a ^2) + (b ^2)) - (((2 * a) * b) * (cos (angle (p1,p2,p3))))