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

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

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

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

end;

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

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

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

( (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 A20, SIN_COS6:21;
hence |.(p2 - p3).| * |.(p4 - p6).| = |.(p3 - p1).| * |.(p5 - p4).| by A3, A4, A9, COMPLEX2:101; :: thesis: verum

end;

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

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

end;

end;

end;

end;