let p1, p2, p3, p4, p5, p6 be Point of (TOP-REAL 2); ( p1,p2,p3 is_a_triangle & p4,p5,p6 is_a_triangle & 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).| & |.(p3 - p2).| * |.(p5 - p4).| = |.(p2 - p1).| * |.(p6 - p5).| & |.(p1 - p3).| * |.(p5 - p4).| = |.(p2 - p1).| * |.(p4 - p6).| ) )
assume
p1,p2,p3 is_a_triangle
; ( not p4,p5,p6 is_a_triangle 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).| & |.(p3 - p2).| * |.(p5 - p4).| = |.(p2 - p1).| * |.(p6 - p5).| & |.(p1 - p3).| * |.(p5 - p4).| = |.(p2 - p1).| * |.(p4 - p6).| ) )
then A1:
p1,p2,p3 are_mutually_distinct
by Th20;
then A2:
p3 <> p2
by ZFMISC_1:def 5;
A3:
p2 <> p1
by A1, ZFMISC_1:def 5;
then A4:
euc2cpx p2 <> euc2cpx p1
by EUCLID_3:4;
A5:
p3 <> p1
by A1, ZFMISC_1:def 5;
then A6:
euc2cpx p3 <> euc2cpx p1
by EUCLID_3:4;
assume A7:
p4,p5,p6 is_a_triangle
; ( 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).| & |.(p3 - p2).| * |.(p5 - p4).| = |.(p2 - p1).| * |.(p6 - p5).| & |.(p1 - p3).| * |.(p5 - p4).| = |.(p2 - p1).| * |.(p4 - p6).| ) )
then A8:
( angle (p4,p5,p6) <> PI & angle (p5,p6,p4) <> PI )
by Th20;
A9:
p4,p5,p6 are_mutually_distinct
by A7, Th20;
then A10:
p5 <> p6
by ZFMISC_1:def 5;
then A11:
euc2cpx p5 <> euc2cpx p6
by EUCLID_3:4;
A12:
p6 <> p4
by A9, ZFMISC_1:def 5;
then A13:
euc2cpx p6 <> euc2cpx p4
by EUCLID_3:4;
A14:
p5 <> p4
by A9, ZFMISC_1:def 5;
then A15:
euc2cpx p5 <> euc2cpx p4
by EUCLID_3:4;
assume A16:
( angle (p1,p2,p3) = angle (p4,p5,p6) & angle (p3,p1,p2) = angle (p6,p4,p5) )
; ( |.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).| & |.(p3 - p2).| * |.(p5 - p4).| = |.(p2 - p1).| * |.(p6 - p5).| & |.(p1 - p3).| * |.(p5 - p4).| = |.(p2 - p1).| * |.(p4 - p6).| )
A17:
euc2cpx p3 <> euc2cpx p2
by A2, EUCLID_3:4;
A18:
angle (p2,p3,p1) = angle (p5,p6,p4)
proof
per cases
( ( ((angle (p3,p1,p2)) + (angle (p1,p2,p3))) + (angle (p2,p3,p1)) = PI & ((angle (p6,p4,p5)) + (angle (p4,p5,p6))) + (angle (p5,p6,p4)) = PI ) or ( ((angle (p3,p1,p2)) + (angle (p1,p2,p3))) + (angle (p2,p3,p1)) = 5 * PI & ((angle (p6,p4,p5)) + (angle (p4,p5,p6))) + (angle (p5,p6,p4)) = 5 * PI ) or ( ((angle (p3,p1,p2)) + (angle (p1,p2,p3))) + (angle (p2,p3,p1)) = PI & ((angle (p6,p4,p5)) + (angle (p4,p5,p6))) + (angle (p5,p6,p4)) = 5 * PI ) or ( ((angle (p3,p1,p2)) + (angle (p1,p2,p3))) + (angle (p2,p3,p1)) = 5 * PI & ((angle (p6,p4,p5)) + (angle (p4,p5,p6))) + (angle (p5,p6,p4)) = PI ) )
by A17, A6, A4, A11, A15, A13, COMPLEX2:88;
suppose
(
((angle (p3,p1,p2)) + (angle (p1,p2,p3))) + (angle (p2,p3,p1)) = PI &
((angle (p6,p4,p5)) + (angle (p4,p5,p6))) + (angle (p5,p6,p4)) = PI )
;
angle (p2,p3,p1) = angle (p5,p6,p4)end; suppose
(
((angle (p3,p1,p2)) + (angle (p1,p2,p3))) + (angle (p2,p3,p1)) = 5
* PI &
((angle (p6,p4,p5)) + (angle (p4,p5,p6))) + (angle (p5,p6,p4)) = 5
* PI )
;
angle (p2,p3,p1) = angle (p5,p6,p4)end; suppose A19:
(
((angle (p3,p1,p2)) + (angle (p1,p2,p3))) + (angle (p2,p3,p1)) = PI &
((angle (p6,p4,p5)) + (angle (p4,p5,p6))) + (angle (p5,p6,p4)) = 5
* PI )
;
angle (p2,p3,p1) = angle (p5,p6,p4)
(
angle (
p2,
p3,
p1)
>= 0 &
- (angle (p5,p6,p4)) > - (2 * PI) )
by COMPLEX2:70, XREAL_1:24;
then A20:
(angle (p2,p3,p1)) + (- (angle (p5,p6,p4))) > 0 + (- (2 * PI))
by XREAL_1:8;
(angle (p2,p3,p1)) - (angle (p5,p6,p4)) = - (4 * PI)
by A16, A19;
then
4
* PI < 2
* PI
by A20, XREAL_1:24;
then
(4 * PI) / PI < (2 * PI) / PI
by XREAL_1:74;
then
4
< (2 * PI) / PI
by XCMPLX_1:89;
then
4
< 2
by XCMPLX_1:89;
hence
angle (
p2,
p3,
p1)
= angle (
p5,
p6,
p4)
;
verum end; suppose A21:
(
((angle (p3,p1,p2)) + (angle (p1,p2,p3))) + (angle (p2,p3,p1)) = 5
* PI &
((angle (p6,p4,p5)) + (angle (p4,p5,p6))) + (angle (p5,p6,p4)) = PI )
;
angle (p2,p3,p1) = angle (p5,p6,p4)
(
angle (
p2,
p3,
p1)
< 2
* PI &
angle (
p5,
p6,
p4)
>= 0 )
by COMPLEX2:70;
then
(angle (p2,p3,p1)) + (- (angle (p5,p6,p4))) < (2 * PI) + (- 0)
by XREAL_1:8;
then
(4 * PI) / PI < (2 * PI) / PI
by A16, A21, XREAL_1:74;
then
4
< (2 * PI) / PI
by XCMPLX_1:89;
then
4
< 2
by XCMPLX_1:89;
hence
angle (
p2,
p3,
p1)
= angle (
p5,
p6,
p4)
;
verum end; end;
end;
A22:
angle (p6,p4,p5) <> PI
by A7, Th20;
hence
|.(p3 - p2).| * |.(p4 - p6).| = |.(p1 - p3).| * |.(p6 - p5).|
by A2, A5, A3, A8, A10, A14, A12, A16, A18, Lm18; ( |.(p3 - p2).| * |.(p5 - p4).| = |.(p2 - p1).| * |.(p6 - p5).| & |.(p1 - p3).| * |.(p5 - p4).| = |.(p2 - p1).| * |.(p4 - p6).| )
thus
|.(p3 - p2).| * |.(p5 - p4).| = |.(p2 - p1).| * |.(p6 - p5).|
by A2, A5, A3, A8, A22, A10, A14, A12, A16, A18, Lm18; |.(p1 - p3).| * |.(p5 - p4).| = |.(p2 - p1).| * |.(p4 - p6).|
thus
|.(p1 - p3).| * |.(p5 - p4).| = |.(p2 - p1).| * |.(p4 - p6).|
by A2, A5, A3, A8, A22, A10, A14, A12, A16, A18, Lm18; verum