let p1, p2, p3 be Point of (TOP-REAL 2); :: thesis: ( p1 <> p2 & p3 <> p2 & ( angle (p1,p2,p3) = PI / 2 or angle (p1,p2,p3) = (3 / 2) * PI ) implies (|.(p1 - p2).| ^2) + (|.(p3 - p2).| ^2) = |.(p1 - p3).| ^2 )
assume that
A1: ( p1 <> p2 & p3 <> p2 ) and
A2: ( angle (p1,p2,p3) = PI / 2 or angle (p1,p2,p3) = (3 / 2) * PI ) ; :: thesis: (|.(p1 - p2).| ^2) + (|.(p3 - p2).| ^2) = |.(p1 - p3).| ^2
A3: ( (euc2cpx p1) - (euc2cpx p2) = euc2cpx (p1 - p2) & (euc2cpx p3) - (euc2cpx p2) = euc2cpx (p3 - p2) ) by Th15;
A4: ( (euc2cpx p1) - (euc2cpx p3) = euc2cpx (p1 - p3) & |.(euc2cpx (p1 - p2)).| = |.(p1 - p2).| ) by Th15, Th25;
A5: ( |.(euc2cpx (p3 - p2)).| = |.(p3 - p2).| & |.(euc2cpx (p1 - p3)).| = |.(p1 - p3).| ) by Th25;
( euc2cpx p1 <> euc2cpx p2 & euc2cpx p3 <> euc2cpx p2 ) by A1, Th4;
hence (|.(p1 - p2).| ^2) + (|.(p3 - p2).| ^2) = |.(p1 - p3).| ^2 by A2, A3, A4, A5, COMPLEX2:77; :: thesis: verum