theorem :: EUCLID_6:50

for p1, p2, p3 being Point of (TOP-REAL 2)
for c1, c2 being Element of COMPLEX st c1 = euc2cpx (p1 - p2) & c2 = euc2cpx (p3 - p2) holds
( Re (c1 .|. c2) = (((p1 `1) - (p2 `1)) * ((p3 `1) - (p2 `1))) + (((p1 `2) - (p2 `2)) * ((p3 `2) - (p2 `2))) & Im (c1 .|. c2) = (- (((p1 `1) - (p2 `1)) * ((p3 `2) - (p2 `2)))) + (((p1 `2) - (p2 `2)) * ((p3 `1) - (p2 `1))) & |.c1.| = sqrt ((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2)) & |.(p1 - p2).| = |.c1.| ) by Lm16;