let p1, p2, p3, p be Point of (TOP-REAL 2); ( p in LSeg (p1,p2) & not p3 in LSeg (p1,p2) & angle (p1,p3,p2) <= PI implies angle (p,p3,p2) <= angle (p1,p3,p2) )
assume A1:
p in LSeg (p1,p2)
; ( p3 in LSeg (p1,p2) or not angle (p1,p3,p2) <= PI or angle (p,p3,p2) <= angle (p1,p3,p2) )
assume A2:
not p3 in LSeg (p1,p2)
; ( not angle (p1,p3,p2) <= PI or angle (p,p3,p2) <= angle (p1,p3,p2) )
assume A3:
angle (p1,p3,p2) <= PI
; angle (p,p3,p2) <= angle (p1,p3,p2)
assume A4:
angle (p,p3,p2) > angle (p1,p3,p2)
; contradiction
per cases
( p = p1 or p = p2 or p1 = p2 or ( p <> p2 & p1 <> p2 & p <> p1 ) )
;
suppose
p = p1
;
contradictionhence
contradiction
by A4;
verum end; suppose A6:
(
p <> p2 &
p1 <> p2 &
p <> p1 )
;
contradictionthen A7:
euc2cpx p <> euc2cpx p1
by EUCLID_3:4;
A8:
p3 <> p1
by A2, RLTOPSP1:68;
then A9:
euc2cpx p3 <> euc2cpx p1
by EUCLID_3:4;
A10:
(
euc2cpx p2 <> euc2cpx p1 &
euc2cpx p <> euc2cpx p2 )
by A6, EUCLID_3:4;
A11:
euc2cpx p <> euc2cpx p3
by A1, A2, EUCLID_3:4;
A12:
angle (
p3,
p2,
p1)
= angle (
p3,
p2,
p)
by A1, A6, Th10;
A13:
p3 <> p2
by A2, RLTOPSP1:68;
then A14:
euc2cpx p3 <> euc2cpx p2
by EUCLID_3:4;
(angle (p1,p3,p2)) + (angle (p2,p1,p3)) = (angle (p,p3,p2)) + (angle (p2,p,p3))
proof
per cases
( ( ((angle (p1,p3,p2)) + (angle (p3,p2,p1))) + (angle (p2,p1,p3)) = PI & ((angle (p,p3,p2)) + (angle (p3,p2,p))) + (angle (p2,p,p3)) = PI ) or ( ((angle (p1,p3,p2)) + (angle (p3,p2,p1))) + (angle (p2,p1,p3)) = 5 * PI & ((angle (p,p3,p2)) + (angle (p3,p2,p))) + (angle (p2,p,p3)) = 5 * PI ) or ( ((angle (p1,p3,p2)) + (angle (p3,p2,p1))) + (angle (p2,p1,p3)) = PI & ((angle (p,p3,p2)) + (angle (p3,p2,p))) + (angle (p2,p,p3)) = 5 * PI ) or ( ((angle (p1,p3,p2)) + (angle (p3,p2,p1))) + (angle (p2,p1,p3)) = 5 * PI & ((angle (p,p3,p2)) + (angle (p3,p2,p))) + (angle (p2,p,p3)) = PI ) )
by A14, A9, A11, A10, COMPLEX2:88;
suppose
(
((angle (p1,p3,p2)) + (angle (p3,p2,p1))) + (angle (p2,p1,p3)) = PI &
((angle (p,p3,p2)) + (angle (p3,p2,p))) + (angle (p2,p,p3)) = PI )
;
(angle (p1,p3,p2)) + (angle (p2,p1,p3)) = (angle (p,p3,p2)) + (angle (p2,p,p3))end; suppose
(
((angle (p1,p3,p2)) + (angle (p3,p2,p1))) + (angle (p2,p1,p3)) = 5
* PI &
((angle (p,p3,p2)) + (angle (p3,p2,p))) + (angle (p2,p,p3)) = 5
* PI )
;
(angle (p1,p3,p2)) + (angle (p2,p1,p3)) = (angle (p,p3,p2)) + (angle (p2,p,p3))end; suppose A15:
(
((angle (p1,p3,p2)) + (angle (p3,p2,p1))) + (angle (p2,p1,p3)) = PI &
((angle (p,p3,p2)) + (angle (p3,p2,p))) + (angle (p2,p,p3)) = 5
* PI )
;
(angle (p1,p3,p2)) + (angle (p2,p1,p3)) = (angle (p,p3,p2)) + (angle (p2,p,p3))A16:
(
angle (
p1,
p3,
p2)
>= 0 &
angle (
p2,
p1,
p3)
>= 0 )
by COMPLEX2:70;
angle (
p2,
p,
p3)
< 2
* PI
by COMPLEX2:70;
then A17:
- (angle (p2,p,p3)) > - (2 * PI)
by XREAL_1:24;
angle (
p,
p3,
p2)
< 2
* PI
by COMPLEX2:70;
then
- (angle (p,p3,p2)) > - (2 * PI)
by XREAL_1:24;
then
(- (angle (p,p3,p2))) + (- (angle (p2,p,p3))) > (- (2 * PI)) + (- (2 * PI))
by A17, XREAL_1:8;
then
((angle (p1,p3,p2)) + (angle (p2,p1,p3))) + ((- (angle (p,p3,p2))) - (angle (p2,p,p3))) > (0 + 0) + ((- (2 * PI)) - (2 * PI))
by A16, XREAL_1:8;
hence
(angle (p1,p3,p2)) + (angle (p2,p1,p3)) = (angle (p,p3,p2)) + (angle (p2,p,p3))
by A12, A15;
verum end; suppose A18:
(
((angle (p1,p3,p2)) + (angle (p3,p2,p1))) + (angle (p2,p1,p3)) = 5
* PI &
((angle (p,p3,p2)) + (angle (p3,p2,p))) + (angle (p2,p,p3)) = PI )
;
(angle (p1,p3,p2)) + (angle (p2,p1,p3)) = (angle (p,p3,p2)) + (angle (p2,p,p3))
(
angle (
p2,
p1,
p3)
< 2
* PI &
angle (
p1,
p3,
p2)
< 2
* PI )
by COMPLEX2:70;
then A19:
(angle (p2,p1,p3)) + (angle (p1,p3,p2)) < (2 * PI) + (2 * PI)
by XREAL_1:8;
(
angle (
p,
p3,
p2)
>= 0 &
angle (
p2,
p,
p3)
>= 0 )
by COMPLEX2:70;
then
((angle (p2,p1,p3)) + (angle (p1,p3,p2))) + ((- (angle (p,p3,p2))) - (angle (p2,p,p3))) < ((2 * PI) + (2 * PI)) + (0 + 0)
by A19, XREAL_1:8;
hence
(angle (p1,p3,p2)) + (angle (p2,p1,p3)) = (angle (p,p3,p2)) + (angle (p2,p,p3))
by A12, A18;
verum end; end;
end; then A20:
angle (
p2,
p1,
p3)
> angle (
p2,
p,
p3)
by A4, XREAL_1:8;
per cases
( ( (angle (p2,p,p3)) + (angle (p3,p,p1)) = PI & ((angle (p3,p,p1)) + (angle (p,p1,p3))) + (angle (p1,p3,p)) = PI ) or ( (angle (p2,p,p3)) + (angle (p3,p,p1)) = 3 * PI & ((angle (p3,p,p1)) + (angle (p,p1,p3))) + (angle (p1,p3,p)) = PI ) or ( (angle (p2,p,p3)) + (angle (p3,p,p1)) = PI & ((angle (p3,p,p1)) + (angle (p,p1,p3))) + (angle (p1,p3,p)) = 5 * PI ) or ( (angle (p2,p,p3)) + (angle (p3,p,p1)) = 3 * PI & ((angle (p3,p,p1)) + (angle (p,p1,p3))) + (angle (p1,p3,p)) = 5 * PI ) )
by A1, A6, A9, A11, A7, Th13, COMPLEX2:88;
suppose
(
(angle (p2,p,p3)) + (angle (p3,p,p1)) = PI &
((angle (p3,p,p1)) + (angle (p,p1,p3))) + (angle (p1,p3,p)) = PI )
;
contradictionthen
(angle (p1,p3,p)) + (angle (p,p1,p3)) < 0 + (angle (p,p1,p3))
by A1, A20, Th9;
then
angle (
p1,
p3,
p)
< 0
by XREAL_1:6;
hence
contradiction
by COMPLEX2:70;
verum end; suppose A21:
(
(angle (p2,p,p3)) + (angle (p3,p,p1)) = 3
* PI &
((angle (p3,p,p1)) + (angle (p,p1,p3))) + (angle (p1,p3,p)) = PI )
;
contradictionA22:
(
angle (
p,
p1,
p3)
>= 0 &
angle (
p1,
p3,
p)
>= 0 )
by COMPLEX2:70;
angle (
p2,
p,
p3)
= ((angle (p,p1,p3)) + (angle (p1,p3,p))) + (2 * PI)
by A21;
then
angle (
p2,
p,
p3)
>= 0 + (2 * PI)
by A22, XREAL_1:6;
hence
contradiction
by COMPLEX2:70;
verum end; suppose A23:
(
(angle (p2,p,p3)) + (angle (p3,p,p1)) = PI &
((angle (p3,p,p1)) + (angle (p,p1,p3))) + (angle (p1,p3,p)) = 5
* PI )
;
contradiction
(
angle (
p,
p1,
p3)
< 2
* PI &
angle (
p1,
p3,
p)
< 2
* PI )
by COMPLEX2:70;
then
(angle (p,p1,p3)) + (angle (p1,p3,p)) < (2 * PI) + (2 * PI)
by XREAL_1:8;
then
(angle (p2,p,p3)) + (4 * PI) < 0 + (4 * PI)
by A23;
then
angle (
p2,
p,
p3)
< 0
by XREAL_1:6;
hence
contradiction
by COMPLEX2:70;
verum end; suppose A24:
(
(angle (p2,p,p3)) + (angle (p3,p,p1)) = 3
* PI &
((angle (p3,p,p1)) + (angle (p,p1,p3))) + (angle (p1,p3,p)) = 5
* PI )
;
contradiction
p1,
p3,
p2 are_mutually_distinct
by A6, A8, A13, ZFMISC_1:def 5;
then
angle (
p2,
p1,
p3)
<= PI
by A3, Th23;
then A25:
angle (
p,
p1,
p3)
<= PI
by A1, A6, Th9;
p,
p1,
p3 are_mutually_distinct
by A1, A2, A6, A8, ZFMISC_1:def 5;
then
(
angle (
p1,
p3,
p)
<= PI &
angle (
p3,
p,
p1)
<= PI )
by A25, Th23;
then
(angle (p3,p,p1)) + (angle (p1,p3,p)) <= PI + PI
by XREAL_1:7;
then
((angle (p3,p,p1)) + (angle (p1,p3,p))) + (angle (p,p1,p3)) <= (2 * PI) + PI
by A25, XREAL_1:7;
hence
contradiction
by A24, XREAL_1:68;
verum end; end; end; end;