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 A1: ( p3 <> p2 & p3 <> p1 & 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).| )
then A2: ( euc2cpx p3 <> euc2cpx p2 & euc2cpx p3 <> euc2cpx p1 & euc2cpx p2 <> euc2cpx p1 ) by EUCLID_3:6;
assume A3: ( p5 <> p6 & p5 <> p4 & 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).| )
then A4: ( euc2cpx p5 <> euc2cpx p6 & euc2cpx p5 <> euc2cpx p4 & euc2cpx p6 <> euc2cpx p4 ) by EUCLID_3:6;
assume A5: ( 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 A6: ( 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 A7: ( angle p1,p2,p3 = angle p4,p5,p6 & angle p3,p1,p2 = angle p6,p4,p5 ) ; :: thesis: |.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).|
then A8: (sin (angle p2,p1,p3)) * (sin (angle p6,p5,p4)) = (sin (angle p2,p1,p3)) * (- (sin (angle p1,p2,p3))) by Th2
.= (- (sin (angle p6,p4,p5))) * (- (sin (angle p1,p2,p3))) by A7, 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 A9: (sin (angle p3,p2,p1)) * (sin (angle p5,p4,p6)) <> 0 ; :: thesis: |.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).|

A10: ((|.(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 A1, 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 A3, 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 A9, 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 A10
.= |.(p3 - p1).| * |.(p6 - p5).| by A8, A9, XCMPLX_1:90
.= |.(p1 - p3).| * |.(p6 - p5).| by Lm2 ; :: thesis: verum

end;

suppose A11: (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 A11;

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

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

end;

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

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

end;

end;

end;

end;