let p3, p2, p1, p5, p6, p4 be Point of (TOP-REAL 2); :: thesis: ( p3 <> p2 & p3 <> p1 & p2 <> p1 & p5 <> p6 & p5 <> p4 & p6 <> p4 & angle p1,p2,p3 <> PI & angle p2,p3,p1 <> PI & angle p3,p1,p2 <> PI & angle p4,p5,p6 <> PI & angle p5,p6,p4 <> PI & angle p6,p4,p5 <> PI & angle p1,p2,p3 = angle p4,p5,p6 & angle p3,p1,p2 = angle p6,p4,p5 implies |.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).| )
assume that
A1: ( p3 <> p2 & p3 <> p1 ) and
A2: p2 <> p1 ; :: thesis: ( not p5 <> p6 or not p5 <> p4 or not p6 <> p4 or not angle p1,p2,p3 <> PI or not angle p2,p3,p1 <> PI or not angle p3,p1,p2 <> PI or not angle p4,p5,p6 <> PI or not angle p5,p6,p4 <> PI or not angle p6,p4,p5 <> PI or not angle p1,p2,p3 = angle p4,p5,p6 or not angle p3,p1,p2 = angle p6,p4,p5 or |.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).| )
A3: ( euc2cpx p3 <> euc2cpx p2 & euc2cpx p3 <> euc2cpx p1 ) by A1, EUCLID_3:6;
A4: euc2cpx p2 <> euc2cpx p1 by A2, EUCLID_3:6;
assume that
A5: p5 <> p6 and
A6: p5 <> p4 and
A7: p6 <> p4 ; :: thesis: ( not angle p1,p2,p3 <> PI or not angle p2,p3,p1 <> PI or not angle p3,p1,p2 <> PI or not angle p4,p5,p6 <> PI or not angle p5,p6,p4 <> PI or not angle p6,p4,p5 <> PI or not angle p1,p2,p3 = angle p4,p5,p6 or not angle p3,p1,p2 = angle p6,p4,p5 or |.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).| )
A8: ( euc2cpx p5 <> euc2cpx p6 & euc2cpx p5 <> euc2cpx p4 ) by A5, A6, EUCLID_3:6;
A9: euc2cpx p6 <> euc2cpx p4 by A7, EUCLID_3:6;
assume A10: ( angle p1,p2,p3 <> PI & angle p2,p3,p1 <> PI & angle p3,p1,p2 <> PI ) ; :: thesis: ( not angle p4,p5,p6 <> PI or not angle p5,p6,p4 <> PI or not angle p6,p4,p5 <> PI or not angle p1,p2,p3 = angle p4,p5,p6 or not angle p3,p1,p2 = angle p6,p4,p5 or |.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).| )
assume A11: ( angle p4,p5,p6 <> PI & angle p5,p6,p4 <> PI & angle p6,p4,p5 <> PI ) ; :: thesis: ( not angle p1,p2,p3 = angle p4,p5,p6 or not angle p3,p1,p2 = angle p6,p4,p5 or |.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).| )
assume that
A12: angle p1,p2,p3 = angle p4,p5,p6 and
A13: angle p3,p1,p2 = angle p6,p4,p5 ; :: thesis: |.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).|
A14: (sin (angle p2,p1,p3)) * (sin (angle p6,p5,p4)) = (sin (angle p2,p1,p3)) * (- (sin (angle p1,p2,p3))) by A12, Th2
.= (- (sin (angle p6,p4,p5))) * (- (sin (angle p1,p2,p3))) by A13, Th2
.= (sin (angle p5,p4,p6)) * (- (sin (angle p1,p2,p3))) by Th2
.= (sin (angle p3,p2,p1)) * (sin (angle p5,p4,p6)) by Th2 ;

per cases ( (sin (angle p3,p2,p1)) * (sin (angle p5,p4,p6)) <> 0 or (sin (angle p3,p2,p1)) * (sin (angle p5,p4,p6)) = 0 ) ;

suppose A15: (sin (angle p3,p2,p1)) * (sin (angle p5,p4,p6)) <> 0 ; :: thesis: |.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).|

A16: ((|.(p3 - p2).| * |.(p4 - p6).|) * (sin (angle p3,p2,p1))) * (sin (angle p5,p4,p6)) = (|.(p3 - p2).| * (sin (angle p3,p2,p1))) * (|.(p4 - p6).| * (sin (angle p5,p4,p6)))
.= (|.(p3 - p1).| * (sin (angle p2,p1,p3))) * (|.(p4 - p6).| * (sin (angle p5,p4,p6))) by A2, Th6
.= (|.(p3 - p1).| * (sin (angle p2,p1,p3))) * (|.(p6 - p4).| * (sin (angle p5,p4,p6))) by Lm2
.= (|.(p3 - p1).| * (sin (angle p2,p1,p3))) * (|.(p6 - p5).| * (sin (angle p6,p5,p4))) by A6, Th6
.= ((|.(p3 - p1).| * |.(p6 - p5).|) * (sin (angle p2,p1,p3))) * (sin (angle p6,p5,p4)) ;
thus |.(p3 - p2).| * |.(p4 - p6).| = ((|.(p3 - p2).| * |.(p4 - p6).|) * ((sin (angle p3,p2,p1)) * (sin (angle p5,p4,p6)))) / ((sin (angle p3,p2,p1)) * (sin (angle p5,p4,p6))) by A15, XCMPLX_1:90
.= ((|.(p3 - p1).| * |.(p6 - p5).|) * ((sin (angle p2,p1,p3)) * (sin (angle p6,p5,p4)))) / ((sin (angle p3,p2,p1)) * (sin (angle p5,p4,p6))) by A16
.= |.(p3 - p1).| * |.(p6 - p5).| by A14, A15, XCMPLX_1:90
.= |.(p1 - p3).| * |.(p6 - p5).| by Lm2 ; :: thesis: verum

end;

suppose A17: (sin (angle p3,p2,p1)) * (sin (angle p5,p4,p6)) = 0 ; :: thesis: |.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).|

per cases ( sin (angle p3,p2,p1) = 0 or sin (angle p5,p4,p6) = 0 ) by A17;

suppose A18: sin (angle p3,p2,p1) = 0 ; :: thesis: |.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).|

A19: ( (2 * PI ) * 0 <= angle p1,p2,p3 & angle p1,p2,p3 < (2 * PI ) + ((2 * PI ) * 0 ) ) by COMPLEX2:84;
- (sin (angle p1,p2,p3)) = 0 by A18, Th2;
then ( angle p1,p2,p3 = (2 * PI ) * 0 or angle p1,p2,p3 = PI + ((2 * PI ) * 0 ) ) by A19, SIN_COS6:21;
hence |.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).| by A3, A4, A10, COMPLEX2:101; :: thesis: verum

end;

suppose A20: sin (angle p5,p4,p6) = 0 ; :: thesis: |.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).|

A21: ( (2 * PI ) * 0 <= angle p6,p4,p5 & angle p6,p4,p5 < (2 * PI ) + ((2 * PI ) * 0 ) ) by COMPLEX2:84;
- (sin (angle p6,p4,p5)) = 0 by A20, Th2;
then ( angle p6,p4,p5 = (2 * PI ) * 0 or angle p6,p4,p5 = PI + ((2 * PI ) * 0 ) ) by A21, SIN_COS6:21;
hence |.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).| by A8, A9, A11, COMPLEX2:101; :: thesis: verum

end;

end;

end;

end;