let p1, p2, p3, 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:4;
A4: euc2cpx p2 <> euc2cpx p1 by A2, EUCLID_3:4;
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:4;
A8: euc2cpx p5 <> euc2cpx p6 by A6, EUCLID_3:4;
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:89
.= ((|.(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:89
.= |.(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:70;
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:87; :: 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:70;
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:82, COMPLEX2:87;
hence |.(p2 - p3).| * |.(p4 - p6).| = |.(p3 - p1).| * |.(p5 - p4).| by A10, A12, COMPLEX2:82; :: thesis: verum

end;

end;

end;

end;