theorem ThLawOfCosines: :: GTARSKI2:13

for a, b, c being POINT of TarskiEuclid2Space holds (dist (c,a)) ^2 = (((dist (a,b)) ^2) + ((dist (b,c)) ^2)) - (((2 * (dist (a,b))) * (dist (b,c))) * (cos (angle ((Tn2TR a),(Tn2TR b),(Tn2TR c)))))