let a, b, c be POINT of TarskiEuclid2Space; :: thesis: (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)))))
set ta = |.((Tn2TR a) - (Tn2TR b)).|;
set tb = |.((Tn2TR c) - (Tn2TR b)).|;
set tc = |.((Tn2TR c) - (Tn2TR a)).|;
( |.((Tn2TR a) - (Tn2TR b)).| = dist (a,b) & |.((Tn2TR c) - (Tn2TR b)).| = dist (c,b) & |.((Tn2TR c) - (Tn2TR a)).| = dist (c,a) ) by ThEquiv;
hence (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))))) by EUCLID_6:7; :: thesis: verum