Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  btwnconn1lem11 Unicode version

Theorem btwnconn1lem11 24720
Description: Lemma for btwnconn1 24724. Now, we establish that  D and  Q are equidistant from  C (Contributed by Scott Fenton, 8-Oct-2013.)
Assertion
Ref Expression
btwnconn1lem11  |-  ( ( ( ( N  e.  NN  /\  A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE
`  N )  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N
) )  /\  (
d  e.  ( EE
`  N )  /\  b  e.  ( EE `  N )  /\  E  e.  ( EE `  N
) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  R  e.  ( EE `  N
) ) )  /\  ( ( ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  c )  /\  ( B  Btwn  <. A ,  C >.  /\  B  Btwn  <. A ,  D >. ) )  /\  ( ( D  Btwn  <. A ,  c >.  /\ 
<. D ,  c >.Cgr <. C ,  D >. )  /\  ( C  Btwn  <. A ,  d >.  /\ 
<. C ,  d >.Cgr <. C ,  D >. ) )  /\  ( ( c  Btwn  <. A , 
b >.  /\  <. c ,  b >.Cgr <. C ,  B >. )  /\  ( d 
Btwn  <. A ,  b
>.  /\  <. d ,  b
>.Cgr <. D ,  B >. ) ) )  /\  ( ( E  Btwn  <. C ,  c >.  /\  E  Btwn  <. D , 
d >. )  /\  (
( C  Btwn  <. c ,  P >.  /\  <. C ,  P >.Cgr <. C ,  d
>. )  /\  ( C  Btwn  <. d ,  R >.  /\  <. C ,  R >.Cgr
<. C ,  E >. )  /\  ( R  Btwn  <. P ,  Q >.  /\ 
<. R ,  Q >.Cgr <. R ,  P >. ) ) ) ) )  ->  <. D ,  C >.Cgr
<. Q ,  C >. )

Proof of Theorem btwnconn1lem11
StepHypRef Expression
1 btwnconn1lem8 24717 . . . . 5  |-  ( ( ( ( N  e.  NN  /\  A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE
`  N )  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N
) )  /\  (
d  e.  ( EE
`  N )  /\  b  e.  ( EE `  N )  /\  E  e.  ( EE `  N
) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  R  e.  ( EE `  N
) ) )  /\  ( ( ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  c )  /\  ( B  Btwn  <. A ,  C >.  /\  B  Btwn  <. A ,  D >. ) )  /\  ( ( D  Btwn  <. A ,  c >.  /\ 
<. D ,  c >.Cgr <. C ,  D >. )  /\  ( C  Btwn  <. A ,  d >.  /\ 
<. C ,  d >.Cgr <. C ,  D >. ) )  /\  ( ( c  Btwn  <. A , 
b >.  /\  <. c ,  b >.Cgr <. C ,  B >. )  /\  ( d 
Btwn  <. A ,  b
>.  /\  <. d ,  b
>.Cgr <. D ,  B >. ) ) )  /\  ( ( E  Btwn  <. C ,  c >.  /\  E  Btwn  <. D , 
d >. )  /\  (
( C  Btwn  <. c ,  P >.  /\  <. C ,  P >.Cgr <. C ,  d
>. )  /\  ( C  Btwn  <. d ,  R >.  /\  <. C ,  R >.Cgr
<. C ,  E >. )  /\  ( R  Btwn  <. P ,  Q >.  /\ 
<. R ,  Q >.Cgr <. R ,  P >. ) ) ) ) )  ->  <. R ,  P >.Cgr
<. E ,  d >.
)
2 btwnconn1lem9 24718 . . . . 5  |-  ( ( ( ( N  e.  NN  /\  A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE
`  N )  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N
) )  /\  (
d  e.  ( EE
`  N )  /\  b  e.  ( EE `  N )  /\  E  e.  ( EE `  N
) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  R  e.  ( EE `  N
) ) )  /\  ( ( ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  c )  /\  ( B  Btwn  <. A ,  C >.  /\  B  Btwn  <. A ,  D >. ) )  /\  ( ( D  Btwn  <. A ,  c >.  /\ 
<. D ,  c >.Cgr <. C ,  D >. )  /\  ( C  Btwn  <. A ,  d >.  /\ 
<. C ,  d >.Cgr <. C ,  D >. ) )  /\  ( ( c  Btwn  <. A , 
b >.  /\  <. c ,  b >.Cgr <. C ,  B >. )  /\  ( d 
Btwn  <. A ,  b
>.  /\  <. d ,  b
>.Cgr <. D ,  B >. ) ) )  /\  ( ( E  Btwn  <. C ,  c >.  /\  E  Btwn  <. D , 
d >. )  /\  (
( C  Btwn  <. c ,  P >.  /\  <. C ,  P >.Cgr <. C ,  d
>. )  /\  ( C  Btwn  <. d ,  R >.  /\  <. C ,  R >.Cgr
<. C ,  E >. )  /\  ( R  Btwn  <. P ,  Q >.  /\ 
<. R ,  Q >.Cgr <. R ,  P >. ) ) ) ) )  ->  <. R ,  Q >.Cgr
<. E ,  D >. )
3 btwnconn1lem10 24719 . . . . 5  |-  ( ( ( ( N  e.  NN  /\  A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE
`  N )  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N
) )  /\  (
d  e.  ( EE
`  N )  /\  b  e.  ( EE `  N )  /\  E  e.  ( EE `  N
) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  R  e.  ( EE `  N
) ) )  /\  ( ( ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  c )  /\  ( B  Btwn  <. A ,  C >.  /\  B  Btwn  <. A ,  D >. ) )  /\  ( ( D  Btwn  <. A ,  c >.  /\ 
<. D ,  c >.Cgr <. C ,  D >. )  /\  ( C  Btwn  <. A ,  d >.  /\ 
<. C ,  d >.Cgr <. C ,  D >. ) )  /\  ( ( c  Btwn  <. A , 
b >.  /\  <. c ,  b >.Cgr <. C ,  B >. )  /\  ( d 
Btwn  <. A ,  b
>.  /\  <. d ,  b
>.Cgr <. D ,  B >. ) ) )  /\  ( ( E  Btwn  <. C ,  c >.  /\  E  Btwn  <. D , 
d >. )  /\  (
( C  Btwn  <. c ,  P >.  /\  <. C ,  P >.Cgr <. C ,  d
>. )  /\  ( C  Btwn  <. d ,  R >.  /\  <. C ,  R >.Cgr
<. C ,  E >. )  /\  ( R  Btwn  <. P ,  Q >.  /\ 
<. R ,  Q >.Cgr <. R ,  P >. ) ) ) ) )  ->  <. d ,  D >.Cgr
<. P ,  Q >. )
41, 2, 33jca 1132 . . . 4  |-  ( ( ( ( N  e.  NN  /\  A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE
`  N )  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N
) )  /\  (
d  e.  ( EE
`  N )  /\  b  e.  ( EE `  N )  /\  E  e.  ( EE `  N
) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  R  e.  ( EE `  N
) ) )  /\  ( ( ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  c )  /\  ( B  Btwn  <. A ,  C >.  /\  B  Btwn  <. A ,  D >. ) )  /\  ( ( D  Btwn  <. A ,  c >.  /\ 
<. D ,  c >.Cgr <. C ,  D >. )  /\  ( C  Btwn  <. A ,  d >.  /\ 
<. C ,  d >.Cgr <. C ,  D >. ) )  /\  ( ( c  Btwn  <. A , 
b >.  /\  <. c ,  b >.Cgr <. C ,  B >. )  /\  ( d 
Btwn  <. A ,  b
>.  /\  <. d ,  b
>.Cgr <. D ,  B >. ) ) )  /\  ( ( E  Btwn  <. C ,  c >.  /\  E  Btwn  <. D , 
d >. )  /\  (
( C  Btwn  <. c ,  P >.  /\  <. C ,  P >.Cgr <. C ,  d
>. )  /\  ( C  Btwn  <. d ,  R >.  /\  <. C ,  R >.Cgr
<. C ,  E >. )  /\  ( R  Btwn  <. P ,  Q >.  /\ 
<. R ,  Q >.Cgr <. R ,  P >. ) ) ) ) )  ->  ( <. R ,  P >.Cgr <. E ,  d
>.  /\  <. R ,  Q >.Cgr
<. E ,  D >.  /\ 
<. d ,  D >.Cgr <. P ,  Q >. ) )
54adantr 451 . . 3  |-  ( ( ( ( ( N  e.  NN  /\  A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE
`  N )  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N
) )  /\  (
d  e.  ( EE
`  N )  /\  b  e.  ( EE `  N )  /\  E  e.  ( EE `  N
) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  R  e.  ( EE `  N
) ) )  /\  ( ( ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  c )  /\  ( B  Btwn  <. A ,  C >.  /\  B  Btwn  <. A ,  D >. ) )  /\  ( ( D  Btwn  <. A ,  c >.  /\ 
<. D ,  c >.Cgr <. C ,  D >. )  /\  ( C  Btwn  <. A ,  d >.  /\ 
<. C ,  d >.Cgr <. C ,  D >. ) )  /\  ( ( c  Btwn  <. A , 
b >.  /\  <. c ,  b >.Cgr <. C ,  B >. )  /\  ( d 
Btwn  <. A ,  b
>.  /\  <. d ,  b
>.Cgr <. D ,  B >. ) ) )  /\  ( ( E  Btwn  <. C ,  c >.  /\  E  Btwn  <. D , 
d >. )  /\  (
( C  Btwn  <. c ,  P >.  /\  <. C ,  P >.Cgr <. C ,  d
>. )  /\  ( C  Btwn  <. d ,  R >.  /\  <. C ,  R >.Cgr
<. C ,  E >. )  /\  ( R  Btwn  <. P ,  Q >.  /\ 
<. R ,  Q >.Cgr <. R ,  P >. ) ) ) ) )  /\  d  =  E )  ->  ( <. R ,  P >.Cgr <. E , 
d >.  /\  <. R ,  Q >.Cgr <. E ,  D >.  /\  <. d ,  D >.Cgr
<. P ,  Q >. ) )
6 simpr3r 1017 . . . . . . 7  |-  ( ( ( E  Btwn  <. C , 
c >.  /\  E  Btwn  <. D ,  d >. )  /\  ( ( C 
Btwn  <. c ,  P >.  /\  <. C ,  P >.Cgr
<. C ,  d >.
)  /\  ( C  Btwn  <. d ,  R >.  /\  <. C ,  R >.Cgr
<. C ,  E >. )  /\  ( R  Btwn  <. P ,  Q >.  /\ 
<. R ,  Q >.Cgr <. R ,  P >. ) ) )  ->  <. R ,  Q >.Cgr <. R ,  P >. )
76adantl 452 . . . . . 6  |-  ( ( ( ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  c )  /\  ( B  Btwn  <. A ,  C >.  /\  B  Btwn  <. A ,  D >. ) )  /\  ( ( D  Btwn  <. A ,  c >.  /\ 
<. D ,  c >.Cgr <. C ,  D >. )  /\  ( C  Btwn  <. A ,  d >.  /\ 
<. C ,  d >.Cgr <. C ,  D >. ) )  /\  ( ( c  Btwn  <. A , 
b >.  /\  <. c ,  b >.Cgr <. C ,  B >. )  /\  ( d 
Btwn  <. A ,  b
>.  /\  <. d ,  b
>.Cgr <. D ,  B >. ) ) )  /\  ( ( E  Btwn  <. C ,  c >.  /\  E  Btwn  <. D , 
d >. )  /\  (
( C  Btwn  <. c ,  P >.  /\  <. C ,  P >.Cgr <. C ,  d
>. )  /\  ( C  Btwn  <. d ,  R >.  /\  <. C ,  R >.Cgr
<. C ,  E >. )  /\  ( R  Btwn  <. P ,  Q >.  /\ 
<. R ,  Q >.Cgr <. R ,  P >. ) ) ) )  ->  <. R ,  Q >.Cgr <. R ,  P >. )
8 simpr2r 1015 . . . . . . 7  |-  ( ( ( E  Btwn  <. C , 
c >.  /\  E  Btwn  <. D ,  d >. )  /\  ( ( C 
Btwn  <. c ,  P >.  /\  <. C ,  P >.Cgr
<. C ,  d >.
)  /\  ( C  Btwn  <. d ,  R >.  /\  <. C ,  R >.Cgr
<. C ,  E >. )  /\  ( R  Btwn  <. P ,  Q >.  /\ 
<. R ,  Q >.Cgr <. R ,  P >. ) ) )  ->  <. C ,  R >.Cgr <. C ,  E >. )
98adantl 452 . . . . . 6  |-  ( ( ( ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  c )  /\  ( B  Btwn  <. A ,  C >.  /\  B  Btwn  <. A ,  D >. ) )  /\  ( ( D  Btwn  <. A ,  c >.  /\ 
<. D ,  c >.Cgr <. C ,  D >. )  /\  ( C  Btwn  <. A ,  d >.  /\ 
<. C ,  d >.Cgr <. C ,  D >. ) )  /\  ( ( c  Btwn  <. A , 
b >.  /\  <. c ,  b >.Cgr <. C ,  B >. )  /\  ( d 
Btwn  <. A ,  b
>.  /\  <. d ,  b
>.Cgr <. D ,  B >. ) ) )  /\  ( ( E  Btwn  <. C ,  c >.  /\  E  Btwn  <. D , 
d >. )  /\  (
( C  Btwn  <. c ,  P >.  /\  <. C ,  P >.Cgr <. C ,  d
>. )  /\  ( C  Btwn  <. d ,  R >.  /\  <. C ,  R >.Cgr
<. C ,  E >. )  /\  ( R  Btwn  <. P ,  Q >.  /\ 
<. R ,  Q >.Cgr <. R ,  P >. ) ) ) )  ->  <. C ,  R >.Cgr <. C ,  E >. )
107, 9jca 518 . . . . 5  |-  ( ( ( ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  c )  /\  ( B  Btwn  <. A ,  C >.  /\  B  Btwn  <. A ,  D >. ) )  /\  ( ( D  Btwn  <. A ,  c >.  /\ 
<. D ,  c >.Cgr <. C ,  D >. )  /\  ( C  Btwn  <. A ,  d >.  /\ 
<. C ,  d >.Cgr <. C ,  D >. ) )  /\  ( ( c  Btwn  <. A , 
b >.  /\  <. c ,  b >.Cgr <. C ,  B >. )  /\  ( d 
Btwn  <. A ,  b
>.  /\  <. d ,  b
>.Cgr <. D ,  B >. ) ) )  /\  ( ( E  Btwn  <. C ,  c >.  /\  E  Btwn  <. D , 
d >. )  /\  (
( C  Btwn  <. c ,  P >.  /\  <. C ,  P >.Cgr <. C ,  d
>. )  /\  ( C  Btwn  <. d ,  R >.  /\  <. C ,  R >.Cgr
<. C ,  E >. )  /\  ( R  Btwn  <. P ,  Q >.  /\ 
<. R ,  Q >.Cgr <. R ,  P >. ) ) ) )  -> 
( <. R ,  Q >.Cgr
<. R ,  P >.  /\ 
<. C ,  R >.Cgr <. C ,  E >. ) )
11 opeq2 3797 . . . . . . . . . . . 12  |-  ( d  =  E  ->  <. C , 
d >.  =  <. C ,  E >. )
1211breq2d 4035 . . . . . . . . . . 11  |-  ( d  =  E  ->  ( <. C ,  R >.Cgr <. C ,  d >.  <->  <. C ,  R >.Cgr <. C ,  E >. ) )
1312anbi2d 684 . . . . . . . . . 10  |-  ( d  =  E  ->  (
( <. R ,  Q >.Cgr
<. R ,  P >.  /\ 
<. C ,  R >.Cgr <. C ,  d >. )  <-> 
( <. R ,  Q >.Cgr
<. R ,  P >.  /\ 
<. C ,  R >.Cgr <. C ,  E >. ) ) )
14 opeq1 3796 . . . . . . . . . . . 12  |-  ( d  =  E  ->  <. d ,  d >.  =  <. E ,  d >. )
1514breq2d 4035 . . . . . . . . . . 11  |-  ( d  =  E  ->  ( <. R ,  P >.Cgr <.
d ,  d >.  <->  <. R ,  P >.Cgr <. E ,  d >. ) )
16 opeq1 3796 . . . . . . . . . . . 12  |-  ( d  =  E  ->  <. d ,  D >.  =  <. E ,  D >. )
1716breq2d 4035 . . . . . . . . . . 11  |-  ( d  =  E  ->  ( <. R ,  Q >.Cgr <.
d ,  D >.  <->  <. R ,  Q >.Cgr <. E ,  D >. ) )
1815, 173anbi12d 1253 . . . . . . . . . 10  |-  ( d  =  E  ->  (
( <. R ,  P >.Cgr
<. d ,  d >.  /\  <. R ,  Q >.Cgr
<. d ,  D >.  /\ 
<. d ,  D >.Cgr <. P ,  Q >. )  <-> 
( <. R ,  P >.Cgr
<. E ,  d >.  /\  <. R ,  Q >.Cgr
<. E ,  D >.  /\ 
<. d ,  D >.Cgr <. P ,  Q >. ) ) )
1913, 18anbi12d 691 . . . . . . . . 9  |-  ( d  =  E  ->  (
( ( <. R ,  Q >.Cgr <. R ,  P >.  /\  <. C ,  R >.Cgr
<. C ,  d >.
)  /\  ( <. R ,  P >.Cgr <. d ,  d >.  /\  <. R ,  Q >.Cgr <. d ,  D >.  /\  <. d ,  D >.Cgr <. P ,  Q >. ) )  <->  ( ( <. R ,  Q >.Cgr <. R ,  P >.  /\ 
<. C ,  R >.Cgr <. C ,  E >. )  /\  ( <. R ,  P >.Cgr <. E ,  d
>.  /\  <. R ,  Q >.Cgr
<. E ,  D >.  /\ 
<. d ,  D >.Cgr <. P ,  Q >. ) ) ) )
2019biimpar 471 . . . . . . . 8  |-  ( ( d  =  E  /\  ( ( <. R ,  Q >.Cgr <. R ,  P >.  /\  <. C ,  R >.Cgr
<. C ,  E >. )  /\  ( <. R ,  P >.Cgr <. E ,  d
>.  /\  <. R ,  Q >.Cgr
<. E ,  D >.  /\ 
<. d ,  D >.Cgr <. P ,  Q >. ) ) )  ->  (
( <. R ,  Q >.Cgr
<. R ,  P >.  /\ 
<. C ,  R >.Cgr <. C ,  d >. )  /\  ( <. R ,  P >.Cgr <. d ,  d
>.  /\  <. R ,  Q >.Cgr
<. d ,  D >.  /\ 
<. d ,  D >.Cgr <. P ,  Q >. ) ) )
21 simpr1 961 . . . . . . . . . 10  |-  ( ( ( <. R ,  Q >.Cgr
<. R ,  P >.  /\ 
<. C ,  R >.Cgr <. C ,  d >. )  /\  ( <. R ,  P >.Cgr <. d ,  d
>.  /\  <. R ,  Q >.Cgr
<. d ,  D >.  /\ 
<. d ,  D >.Cgr <. P ,  Q >. ) )  ->  <. R ,  P >.Cgr <. d ,  d
>. )
22 simp11 985 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  N  e.  NN )
23 simp33 993 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  R  e.  ( EE `  N
) )
24 simp31 991 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  P  e.  ( EE `  N
) )
25 simp2r1 1057 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  d  e.  ( EE `  N
) )
26 axcgrid 24544 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  ( R  e.  ( EE `  N )  /\  P  e.  ( EE `  N )  /\  d  e.  ( EE `  N
) ) )  -> 
( <. R ,  P >.Cgr
<. d ,  d >.  ->  R  =  P ) )
2722, 23, 24, 25, 26syl13anc 1184 . . . . . . . . . 10  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  ( <. R ,  P >.Cgr <.
d ,  d >.  ->  R  =  P ) )
2821, 27syl5 28 . . . . . . . . 9  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  (
( ( <. R ,  Q >.Cgr <. R ,  P >.  /\  <. C ,  R >.Cgr
<. C ,  d >.
)  /\  ( <. R ,  P >.Cgr <. d ,  d >.  /\  <. R ,  Q >.Cgr <. d ,  D >.  /\  <. d ,  D >.Cgr <. P ,  Q >. ) )  ->  R  =  P ) )
29 opeq1 3796 . . . . . . . . . . . . . . 15  |-  ( R  =  P  ->  <. R ,  Q >.  =  <. P ,  Q >. )
30 opeq1 3796 . . . . . . . . . . . . . . 15  |-  ( R  =  P  ->  <. R ,  P >.  =  <. P ,  P >. )
3129, 30breq12d 4036 . . . . . . . . . . . . . 14  |-  ( R  =  P  ->  ( <. R ,  Q >.Cgr <. R ,  P >.  <->  <. P ,  Q >.Cgr <. P ,  P >. ) )
32 opeq2 3797 . . . . . . . . . . . . . . 15  |-  ( R  =  P  ->  <. C ,  R >.  =  <. C ,  P >. )
3332breq1d 4033 . . . . . . . . . . . . . 14  |-  ( R  =  P  ->  ( <. C ,  R >.Cgr <. C ,  d >.  <->  <. C ,  P >.Cgr <. C , 
d >. ) )
3431, 33anbi12d 691 . . . . . . . . . . . . 13  |-  ( R  =  P  ->  (
( <. R ,  Q >.Cgr
<. R ,  P >.  /\ 
<. C ,  R >.Cgr <. C ,  d >. )  <-> 
( <. P ,  Q >.Cgr
<. P ,  P >.  /\ 
<. C ,  P >.Cgr <. C ,  d >. ) ) )
3530breq1d 4033 . . . . . . . . . . . . . 14  |-  ( R  =  P  ->  ( <. R ,  P >.Cgr <.
d ,  d >.  <->  <. P ,  P >.Cgr <.
d ,  d >.
) )
3629breq1d 4033 . . . . . . . . . . . . . 14  |-  ( R  =  P  ->  ( <. R ,  Q >.Cgr <.
d ,  D >.  <->  <. P ,  Q >.Cgr <. d ,  D >. ) )
3735, 363anbi12d 1253 . . . . . . . . . . . . 13  |-  ( R  =  P  ->  (
( <. R ,  P >.Cgr
<. d ,  d >.  /\  <. R ,  Q >.Cgr
<. d ,  D >.  /\ 
<. d ,  D >.Cgr <. P ,  Q >. )  <-> 
( <. P ,  P >.Cgr
<. d ,  d >.  /\  <. P ,  Q >.Cgr
<. d ,  D >.  /\ 
<. d ,  D >.Cgr <. P ,  Q >. ) ) )
3834, 37anbi12d 691 . . . . . . . . . . . 12  |-  ( R  =  P  ->  (
( ( <. R ,  Q >.Cgr <. R ,  P >.  /\  <. C ,  R >.Cgr
<. C ,  d >.
)  /\  ( <. R ,  P >.Cgr <. d ,  d >.  /\  <. R ,  Q >.Cgr <. d ,  D >.  /\  <. d ,  D >.Cgr <. P ,  Q >. ) )  <->  ( ( <. P ,  Q >.Cgr <. P ,  P >.  /\ 
<. C ,  P >.Cgr <. C ,  d >. )  /\  ( <. P ,  P >.Cgr <. d ,  d
>.  /\  <. P ,  Q >.Cgr
<. d ,  D >.  /\ 
<. d ,  D >.Cgr <. P ,  Q >. ) ) ) )
3938biimpac 472 . . . . . . . . . . 11  |-  ( ( ( ( <. R ,  Q >.Cgr <. R ,  P >.  /\  <. C ,  R >.Cgr
<. C ,  d >.
)  /\  ( <. R ,  P >.Cgr <. d ,  d >.  /\  <. R ,  Q >.Cgr <. d ,  D >.  /\  <. d ,  D >.Cgr <. P ,  Q >. ) )  /\  R  =  P )  ->  (
( <. P ,  Q >.Cgr
<. P ,  P >.  /\ 
<. C ,  P >.Cgr <. C ,  d >. )  /\  ( <. P ,  P >.Cgr <. d ,  d
>.  /\  <. P ,  Q >.Cgr
<. d ,  D >.  /\ 
<. d ,  D >.Cgr <. P ,  Q >. ) ) )
40 simpll 730 . . . . . . . . . . . . 13  |-  ( ( ( <. P ,  Q >.Cgr
<. P ,  P >.  /\ 
<. C ,  P >.Cgr <. C ,  d >. )  /\  ( <. P ,  P >.Cgr <. d ,  d
>.  /\  <. P ,  Q >.Cgr
<. d ,  D >.  /\ 
<. d ,  D >.Cgr <. P ,  Q >. ) )  ->  <. P ,  Q >.Cgr <. P ,  P >. )
41 simp32 992 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  Q  e.  ( EE `  N
) )
42 axcgrid 24544 . . . . . . . . . . . . . 14  |-  ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  P  e.  ( EE `  N
) ) )  -> 
( <. P ,  Q >.Cgr
<. P ,  P >.  ->  P  =  Q )
)
4322, 24, 41, 24, 42syl13anc 1184 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  ( <. P ,  Q >.Cgr <. P ,  P >.  ->  P  =  Q )
)
4440, 43syl5 28 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  (
( ( <. P ,  Q >.Cgr <. P ,  P >.  /\  <. C ,  P >.Cgr
<. C ,  d >.
)  /\  ( <. P ,  P >.Cgr <. d ,  d >.  /\  <. P ,  Q >.Cgr <. d ,  D >.  /\  <. d ,  D >.Cgr <. P ,  Q >. ) )  ->  P  =  Q ) )
45 simprlr 739 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( N  e.  NN  /\  A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE
`  N )  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N
) )  /\  (
d  e.  ( EE
`  N )  /\  b  e.  ( EE `  N )  /\  E  e.  ( EE `  N
) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  R  e.  ( EE `  N
) ) )  /\  ( ( <. P ,  P >.Cgr <. P ,  P >.  /\  <. C ,  P >.Cgr
<. C ,  d >.
)  /\  ( <. P ,  P >.Cgr <. d ,  d >.  /\  <. P ,  P >.Cgr <. d ,  D >.  /\  <. d ,  D >.Cgr <. P ,  P >. ) ) )  ->  <. C ,  P >.Cgr <. C ,  d >. )
46 simpr3 963 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( <. P ,  P >.Cgr
<. P ,  P >.  /\ 
<. C ,  P >.Cgr <. C ,  d >. )  /\  ( <. P ,  P >.Cgr <. d ,  d
>.  /\  <. P ,  P >.Cgr
<. d ,  D >.  /\ 
<. d ,  D >.Cgr <. P ,  P >. ) )  ->  <. d ,  D >.Cgr <. P ,  P >. )
47 simp2l2 1055 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  D  e.  ( EE `  N
) )
48 axcgrid 24544 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( N  e.  NN  /\  ( d  e.  ( EE `  N )  /\  D  e.  ( EE `  N )  /\  P  e.  ( EE `  N ) ) )  ->  ( <. d ,  D >.Cgr <. P ,  P >.  -> 
d  =  D ) )
4922, 25, 47, 24, 48syl13anc 1184 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  ( <. d ,  D >.Cgr <. P ,  P >.  -> 
d  =  D ) )
5046, 49syl5 28 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  (
( ( <. P ,  P >.Cgr <. P ,  P >.  /\  <. C ,  P >.Cgr
<. C ,  d >.
)  /\  ( <. P ,  P >.Cgr <. d ,  d >.  /\  <. P ,  P >.Cgr <. d ,  D >.  /\  <. d ,  D >.Cgr <. P ,  P >. ) )  ->  d  =  D ) )
5150imp 418 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( N  e.  NN  /\  A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE
`  N )  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N
) )  /\  (
d  e.  ( EE
`  N )  /\  b  e.  ( EE `  N )  /\  E  e.  ( EE `  N
) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  R  e.  ( EE `  N
) ) )  /\  ( ( <. P ,  P >.Cgr <. P ,  P >.  /\  <. C ,  P >.Cgr
<. C ,  d >.
)  /\  ( <. P ,  P >.Cgr <. d ,  d >.  /\  <. P ,  P >.Cgr <. d ,  D >.  /\  <. d ,  D >.Cgr <. P ,  P >. ) ) )  -> 
d  =  D )
5251opeq2d 3803 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( N  e.  NN  /\  A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE
`  N )  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N
) )  /\  (
d  e.  ( EE
`  N )  /\  b  e.  ( EE `  N )  /\  E  e.  ( EE `  N
) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  R  e.  ( EE `  N
) ) )  /\  ( ( <. P ,  P >.Cgr <. P ,  P >.  /\  <. C ,  P >.Cgr
<. C ,  d >.
)  /\  ( <. P ,  P >.Cgr <. d ,  d >.  /\  <. P ,  P >.Cgr <. d ,  D >.  /\  <. d ,  D >.Cgr <. P ,  P >. ) ) )  ->  <. C ,  d >.  =  <. C ,  D >. )
5352breq2d 4035 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( N  e.  NN  /\  A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE
`  N )  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N
) )  /\  (
d  e.  ( EE
`  N )  /\  b  e.  ( EE `  N )  /\  E  e.  ( EE `  N
) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  R  e.  ( EE `  N
) ) )  /\  ( ( <. P ,  P >.Cgr <. P ,  P >.  /\  <. C ,  P >.Cgr
<. C ,  d >.
)  /\  ( <. P ,  P >.Cgr <. d ,  d >.  /\  <. P ,  P >.Cgr <. d ,  D >.  /\  <. d ,  D >.Cgr <. P ,  P >. ) ) )  -> 
( <. C ,  P >.Cgr
<. C ,  d >.  <->  <. C ,  P >.Cgr <. C ,  D >. ) )
54 simp2l1 1054 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  C  e.  ( EE `  N
) )
55 cgrcomlr 24621 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( N  e.  NN  /\  ( C  e.  ( EE `  N )  /\  P  e.  ( EE `  N ) )  /\  ( C  e.  ( EE `  N )  /\  D  e.  ( EE `  N ) ) )  ->  ( <. C ,  P >.Cgr <. C ,  D >.  <->  <. P ,  C >.Cgr <. D ,  C >. ) )
5622, 54, 24, 54, 47, 55syl122anc 1191 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  ( <. C ,  P >.Cgr <. C ,  D >.  <->  <. P ,  C >.Cgr <. D ,  C >. ) )
57 cgrcom 24613 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  ( D  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) ) )  ->  ( <. P ,  C >.Cgr <. D ,  C >.  <->  <. D ,  C >.Cgr <. P ,  C >. ) )
5822, 24, 54, 47, 54, 57syl122anc 1191 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  ( <. P ,  C >.Cgr <. D ,  C >.  <->  <. D ,  C >.Cgr <. P ,  C >. ) )
5956, 58bitrd 244 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  ( <. C ,  P >.Cgr <. C ,  D >.  <->  <. D ,  C >.Cgr <. P ,  C >. ) )
6059adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( N  e.  NN  /\  A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE
`  N )  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N
) )  /\  (
d  e.  ( EE
`  N )  /\  b  e.  ( EE `  N )  /\  E  e.  ( EE `  N
) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  R  e.  ( EE `  N
) ) )  /\  ( ( <. P ,  P >.Cgr <. P ,  P >.  /\  <. C ,  P >.Cgr
<. C ,  d >.
)  /\  ( <. P ,  P >.Cgr <. d ,  d >.  /\  <. P ,  P >.Cgr <. d ,  D >.  /\  <. d ,  D >.Cgr <. P ,  P >. ) ) )  -> 
( <. C ,  P >.Cgr
<. C ,  D >.  <->  <. D ,  C >.Cgr <. P ,  C >. ) )
6153, 60bitrd 244 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( N  e.  NN  /\  A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE
`  N )  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N
) )  /\  (
d  e.  ( EE
`  N )  /\  b  e.  ( EE `  N )  /\  E  e.  ( EE `  N
) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  R  e.  ( EE `  N
) ) )  /\  ( ( <. P ,  P >.Cgr <. P ,  P >.  /\  <. C ,  P >.Cgr
<. C ,  d >.
)  /\  ( <. P ,  P >.Cgr <. d ,  d >.  /\  <. P ,  P >.Cgr <. d ,  D >.  /\  <. d ,  D >.Cgr <. P ,  P >. ) ) )  -> 
( <. C ,  P >.Cgr
<. C ,  d >.  <->  <. D ,  C >.Cgr <. P ,  C >. ) )
6245, 61mpbid 201 . . . . . . . . . . . . . . 15  |-  ( ( ( ( N  e.  NN  /\  A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE
`  N )  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N
) )  /\  (
d  e.  ( EE
`  N )  /\  b  e.  ( EE `  N )  /\  E  e.  ( EE `  N
) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  R  e.  ( EE `  N
) ) )  /\  ( ( <. P ,  P >.Cgr <. P ,  P >.  /\  <. C ,  P >.Cgr
<. C ,  d >.
)  /\  ( <. P ,  P >.Cgr <. d ,  d >.  /\  <. P ,  P >.Cgr <. d ,  D >.  /\  <. d ,  D >.Cgr <. P ,  P >. ) ) )  ->  <. D ,  C >.Cgr <. P ,  C >. )
6362ex 423 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  (
( ( <. P ,  P >.Cgr <. P ,  P >.  /\  <. C ,  P >.Cgr
<. C ,  d >.
)  /\  ( <. P ,  P >.Cgr <. d ,  d >.  /\  <. P ,  P >.Cgr <. d ,  D >.  /\  <. d ,  D >.Cgr <. P ,  P >. ) )  ->  <. D ,  C >.Cgr <. P ,  C >. ) )
64 opeq2 3797 . . . . . . . . . . . . . . . . . 18  |-  ( P  =  Q  ->  <. P ,  P >.  =  <. P ,  Q >. )
6564breq1d 4033 . . . . . . . . . . . . . . . . 17  |-  ( P  =  Q  ->  ( <. P ,  P >.Cgr <. P ,  P >.  <->  <. P ,  Q >.Cgr <. P ,  P >. ) )
6665anbi1d 685 . . . . . . . . . . . . . . . 16  |-  ( P  =  Q  ->  (
( <. P ,  P >.Cgr
<. P ,  P >.  /\ 
<. C ,  P >.Cgr <. C ,  d >. )  <-> 
( <. P ,  Q >.Cgr
<. P ,  P >.  /\ 
<. C ,  P >.Cgr <. C ,  d >. ) ) )
6764breq1d 4033 . . . . . . . . . . . . . . . . 17  |-  ( P  =  Q  ->  ( <. P ,  P >.Cgr <.
d ,  D >.  <->  <. P ,  Q >.Cgr <. d ,  D >. ) )
6864breq2d 4035 . . . . . . . . . . . . . . . . 17  |-  ( P  =  Q  ->  ( <. d ,  D >.Cgr <. P ,  P >.  <->  <. d ,  D >.Cgr <. P ,  Q >. ) )
6967, 683anbi23d 1255 . . . . . . . . . . . . . . . 16  |-  ( P  =  Q  ->  (
( <. P ,  P >.Cgr
<. d ,  d >.  /\  <. P ,  P >.Cgr
<. d ,  D >.  /\ 
<. d ,  D >.Cgr <. P ,  P >. )  <-> 
( <. P ,  P >.Cgr
<. d ,  d >.  /\  <. P ,  Q >.Cgr
<. d ,  D >.  /\ 
<. d ,  D >.Cgr <. P ,  Q >. ) ) )
7066, 69anbi12d 691 . . . . . . . . . . . . . . 15  |-  ( P  =  Q  ->  (
( ( <. P ,  P >.Cgr <. P ,  P >.  /\  <. C ,  P >.Cgr
<. C ,  d >.
)  /\  ( <. P ,  P >.Cgr <. d ,  d >.  /\  <. P ,  P >.Cgr <. d ,  D >.  /\  <. d ,  D >.Cgr <. P ,  P >. ) )  <->  ( ( <. P ,  Q >.Cgr <. P ,  P >.  /\ 
<. C ,  P >.Cgr <. C ,  d >. )  /\  ( <. P ,  P >.Cgr <. d ,  d
>.  /\  <. P ,  Q >.Cgr
<. d ,  D >.  /\ 
<. d ,  D >.Cgr <. P ,  Q >. ) ) ) )
71 opeq1 3796 . . . . . . . . . . . . . . . 16  |-  ( P  =  Q  ->  <. P ,  C >.  =  <. Q ,  C >. )
7271breq2d 4035 . . . . . . . . . . . . . . 15  |-  ( P  =  Q  ->  ( <. D ,  C >.Cgr <. P ,  C >.  <->  <. D ,  C >.Cgr <. Q ,  C >. ) )
7370, 72imbi12d 311 . . . . . . . . . . . . . 14  |-  ( P  =  Q  ->  (
( ( ( <. P ,  P >.Cgr <. P ,  P >.  /\ 
<. C ,  P >.Cgr <. C ,  d >. )  /\  ( <. P ,  P >.Cgr <. d ,  d
>.  /\  <. P ,  P >.Cgr
<. d ,  D >.  /\ 
<. d ,  D >.Cgr <. P ,  P >. ) )  ->  <. D ,  C >.Cgr <. P ,  C >. )  <->  ( ( (
<. P ,  Q >.Cgr <. P ,  P >.  /\ 
<. C ,  P >.Cgr <. C ,  d >. )  /\  ( <. P ,  P >.Cgr <. d ,  d
>.  /\  <. P ,  Q >.Cgr
<. d ,  D >.  /\ 
<. d ,  D >.Cgr <. P ,  Q >. ) )  ->  <. D ,  C >.Cgr <. Q ,  C >. ) ) )
7463, 73syl5ibcom 211 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  ( P  =  Q  ->  ( ( ( <. P ,  Q >.Cgr <. P ,  P >.  /\  <. C ,  P >.Cgr
<. C ,  d >.
)  /\  ( <. P ,  P >.Cgr <. d ,  d >.  /\  <. P ,  Q >.Cgr <. d ,  D >.  /\  <. d ,  D >.Cgr <. P ,  Q >. ) )  ->  <. D ,  C >.Cgr <. Q ,  C >. ) ) )
7574com23 72 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  (
( ( <. P ,  Q >.Cgr <. P ,  P >.  /\  <. C ,  P >.Cgr
<. C ,  d >.
)  /\  ( <. P ,  P >.Cgr <. d ,  d >.  /\  <. P ,  Q >.Cgr <. d ,  D >.  /\  <. d ,  D >.Cgr <. P ,  Q >. ) )  ->  ( P  =  Q  ->  <. D ,  C >.Cgr <. Q ,  C >. ) ) )
7644, 75mpdd 36 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  (
( ( <. P ,  Q >.Cgr <. P ,  P >.  /\  <. C ,  P >.Cgr
<. C ,  d >.
)  /\  ( <. P ,  P >.Cgr <. d ,  d >.  /\  <. P ,  Q >.Cgr <. d ,  D >.  /\  <. d ,  D >.Cgr <. P ,  Q >. ) )  ->  <. D ,  C >.Cgr <. Q ,  C >. ) )
7739, 76syl5 28 . . . . . . . . . 10  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  (
( ( ( <. R ,  Q >.Cgr <. R ,  P >.  /\ 
<. C ,  R >.Cgr <. C ,  d >. )  /\  ( <. R ,  P >.Cgr <. d ,  d
>.  /\  <. R ,  Q >.Cgr
<. d ,  D >.  /\ 
<. d ,  D >.Cgr <. P ,  Q >. ) )  /\  R  =  P )  ->  <. D ,  C >.Cgr <. Q ,  C >. ) )
7877exp3a 425 . . . . . . . . 9  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  (
( ( <. R ,  Q >.Cgr <. R ,  P >.  /\  <. C ,  R >.Cgr
<. C ,  d >.
)  /\  ( <. R ,  P >.Cgr <. d ,  d >.  /\  <. R ,  Q >.Cgr <. d ,  D >.  /\  <. d ,  D >.Cgr <. P ,  Q >. ) )  ->  ( R  =  P  ->  <. D ,  C >.Cgr <. Q ,  C >. ) ) )
7928, 78mpdd 36 . . . . . . . 8  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  (
( ( <. R ,  Q >.Cgr <. R ,  P >.  /\  <. C ,  R >.Cgr
<. C ,  d >.
)  /\  ( <. R ,  P >.Cgr <. d ,  d >.  /\  <. R ,  Q >.Cgr <. d ,  D >.  /\  <. d ,  D >.Cgr <. P ,  Q >. ) )  ->  <. D ,  C >.Cgr <. Q ,  C >. ) )
8020, 79syl5 28 . . . . . . 7  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  (
( d  =  E  /\  ( ( <. R ,  Q >.Cgr <. R ,  P >.  /\ 
<. C ,  R >.Cgr <. C ,  E >. )  /\  ( <. R ,  P >.Cgr <. E ,  d
>.  /\  <. R ,  Q >.Cgr
<. E ,  D >.  /\ 
<. d ,  D >.Cgr <. P ,  Q >. ) ) )  ->  <. D ,  C >.Cgr <. Q ,  C >. ) )
8180exp4d 592 . . . . . 6  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  (
d  =  E  -> 
( ( <. R ,  Q >.Cgr <. R ,  P >.  /\  <. C ,  R >.Cgr
<. C ,  E >. )  ->  ( ( <. R ,  P >.Cgr <. E ,  d >.  /\ 
<. R ,  Q >.Cgr <. E ,  D >.  /\ 
<. d ,  D >.Cgr <. P ,  Q >. )  ->  <. D ,  C >.Cgr
<. Q ,  C >. ) ) ) )
8281com23 72 . . . . 5  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  (
( <. R ,  Q >.Cgr
<. R ,  P >.  /\ 
<. C ,  R >.Cgr <. C ,  E >. )  ->  ( d  =  E  ->  ( ( <. R ,  P >.Cgr <. E ,  d >.  /\ 
<. R ,  Q >.Cgr <. E ,  D >.  /\ 
<. d ,  D >.Cgr <. P ,  Q >. )  ->  <. D ,  C >.Cgr
<. Q ,  C >. ) ) ) )
8310, 82syl5 28 . . . 4  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  (
( ( ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  c )  /\  ( B  Btwn  <. A ,  C >.  /\  B  Btwn  <. A ,  D >. ) )  /\  ( ( D  Btwn  <. A ,  c >.  /\ 
<. D ,  c >.Cgr <. C ,  D >. )  /\  ( C  Btwn  <. A ,  d >.  /\ 
<. C ,  d >.Cgr <. C ,  D >. ) )  /\  ( ( c  Btwn  <. A , 
b >.  /\  <. c ,  b >.Cgr <. C ,  B >. )  /\  ( d 
Btwn  <. A ,  b
>.  /\  <. d ,  b
>.Cgr <. D ,  B >. ) ) )  /\  ( ( E  Btwn  <. C ,  c >.  /\  E  Btwn  <. D , 
d >. )  /\  (
( C  Btwn  <. c ,  P >.  /\  <. C ,  P >.Cgr <. C ,  d
>. )  /\  ( C  Btwn  <. d ,  R >.  /\  <. C ,  R >.Cgr
<. C ,  E >. )  /\  ( R  Btwn  <. P ,  Q >.  /\ 
<. R ,  Q >.Cgr <. R ,  P >. ) ) ) )  -> 
( d  =  E  ->  ( ( <. R ,  P >.Cgr <. E ,  d >.  /\ 
<. R ,  Q >.Cgr <. E ,  D >.  /\ 
<. d ,  D >.Cgr <. P ,  Q >. )  ->  <. D ,  C >.Cgr
<. Q ,  C >. ) ) ) )
8483imp31 421 . . 3  |-  ( ( ( ( ( N  e.  NN  /\  A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE
`  N )  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N
) )  /\  (
d  e.  ( EE
`  N )  /\  b  e.  ( EE `  N )  /\  E  e.  ( EE `  N
) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  R  e.  ( EE `  N
) ) )  /\  ( ( ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  c )  /\  ( B  Btwn  <. A ,  C >.  /\  B  Btwn  <. A ,  D >. ) )  /\  ( ( D  Btwn  <. A ,  c >.  /\ 
<. D ,  c >.Cgr <. C ,  D >. )  /\  ( C  Btwn  <. A ,  d >.  /\ 
<. C ,  d >.Cgr <. C ,  D >. ) )  /\  ( ( c  Btwn  <. A , 
b >.  /\  <. c ,  b >.Cgr <. C ,  B >. )  /\  ( d 
Btwn  <. A ,  b
>.  /\  <. d ,  b
>.Cgr <. D ,  B >. ) ) )  /\  ( ( E  Btwn  <. C ,  c >.  /\  E  Btwn  <. D , 
d >. )  /\  (
( C  Btwn  <. c ,  P >.  /\  <. C ,  P >.Cgr <. C ,  d
>. )  /\  ( C  Btwn  <. d ,  R >.  /\  <. C ,  R >.Cgr
<. C ,  E >. )  /\  ( R  Btwn  <. P ,  Q >.  /\ 
<. R ,  Q >.Cgr <. R ,  P >. ) ) ) ) )  /\  d  =  E )  ->  ( ( <. R ,  P >.Cgr <. E ,  d >.  /\ 
<. R ,  Q >.Cgr <. E ,  D >.  /\ 
<. d ,  D >.Cgr <. P ,  Q >. )  ->  <. D ,  C >.Cgr
<. Q ,  C >. ) )
855, 84mpd 14 . 2  |-  ( ( ( ( ( N  e.  NN  /\  A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE
`  N )  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N
) )  /\  (
d  e.  ( EE
`  N )  /\  b  e.  ( EE `  N )  /\  E  e.  ( EE `  N
) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  R  e.  ( EE `  N
) ) )  /\  ( ( ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  c )  /\  ( B  Btwn  <. A ,  C >.  /\  B  Btwn  <. A ,  D >. ) )  /\  ( ( D  Btwn  <. A ,  c >.  /\ 
<. D ,  c >.Cgr <. C ,  D >. )  /\  ( C  Btwn  <. A ,  d >.  /\ 
<. C ,  d >.Cgr <. C ,  D >. ) )  /\  ( ( c  Btwn  <. A , 
b >.  /\  <. c ,  b >.Cgr <. C ,  B >. )  /\  ( d 
Btwn  <. A ,  b
>.  /\  <. d ,  b
>.Cgr <. D ,  B >. ) ) )  /\  ( ( E  Btwn  <. C ,  c >.  /\  E  Btwn  <. D , 
d >. )  /\  (
( C  Btwn  <. c ,  P >.  /\  <. C ,  P >.Cgr <. C ,  d
>. )  /\  ( C  Btwn  <. d ,  R >.  /\  <. C ,  R >.Cgr
<. C ,  E >. )  /\  ( R  Btwn  <. P ,  Q >.  /\ 
<. R ,  Q >.Cgr <. R ,  P >. ) ) ) ) )  /\  d  =  E )  ->  <. D ,  C >.Cgr <. Q ,  C >. )
86 simp2r3 1059 . . . . . 6  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  E  e.  ( EE `  N
) )
87 simprlr 739 . . . . . . 7  |-  ( ( ( ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  c )  /\  ( B  Btwn  <. A ,  C >.  /\  B  Btwn  <. A ,  D >. ) )  /\  ( ( D  Btwn  <. A ,  c >.  /\ 
<. D ,  c >.Cgr <. C ,  D >. )  /\  ( C  Btwn  <. A ,  d >.  /\ 
<. C ,  d >.Cgr <. C ,  D >. ) )  /\  ( ( c  Btwn  <. A , 
b >.  /\  <. c ,  b >.Cgr <. C ,  B >. )  /\  ( d 
Btwn  <. A ,  b
>.  /\  <. d ,  b
>.Cgr <. D ,  B >. ) ) )  /\  ( ( E  Btwn  <. C ,  c >.  /\  E  Btwn  <. D , 
d >. )  /\  (
( C  Btwn  <. c ,  P >.  /\  <. C ,  P >.Cgr <. C ,  d
>. )  /\  ( C  Btwn  <. d ,  R >.  /\  <. C ,  R >.Cgr
<. C ,  E >. )  /\  ( R  Btwn  <. P ,  Q >.  /\ 
<. R ,  Q >.Cgr <. R ,  P >. ) ) ) )  ->  E  Btwn  <. D ,  d
>. )
8887adantl 452 . . . . . 6  |-  ( ( ( ( N  e.  NN  /\  A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE
`  N )  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N
) )  /\  (
d  e.  ( EE
`  N )  /\  b  e.  ( EE `  N )  /\  E  e.  ( EE `  N
) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  R  e.  ( EE `  N
) ) )  /\  ( ( ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  c )  /\  ( B  Btwn  <. A ,  C >.  /\  B  Btwn  <. A ,  D >. ) )  /\  ( ( D  Btwn  <. A ,  c >.  /\ 
<. D ,  c >.Cgr <. C ,  D >. )  /\  ( C  Btwn  <. A ,  d >.  /\ 
<. C ,  d >.Cgr <. C ,  D >. ) )  /\  ( ( c  Btwn  <. A , 
b >.  /\  <. c ,  b >.Cgr <. C ,  B >. )  /\  ( d 
Btwn  <. A ,  b
>.  /\  <. d ,  b
>.Cgr <. D ,  B >. ) ) )  /\  ( ( E  Btwn  <. C ,  c >.  /\  E  Btwn  <. D , 
d >. )  /\  (
( C  Btwn  <. c ,  P >.  /\  <. C ,  P >.Cgr <. C ,  d
>. )  /\  ( C  Btwn  <. d ,  R >.  /\  <. C ,  R >.Cgr
<. C ,  E >. )  /\  ( R  Btwn  <. P ,  Q >.  /\ 
<. R ,  Q >.Cgr <. R ,  P >. ) ) ) ) )  ->  E  Btwn  <. D , 
d >. )
8922, 86, 47, 25, 88btwncomand 24638 . . . . 5  |-  ( ( ( ( N  e.  NN  /\  A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE
`  N )  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N
) )  /\  (
d  e.  ( EE
`  N )  /\  b  e.  ( EE `  N )  /\  E  e.  ( EE `  N
) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  R  e.  ( EE `  N
) ) )  /\  ( ( ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  c )  /\  ( B  Btwn  <. A ,  C >.  /\  B  Btwn  <. A ,  D >. ) )  /\  ( ( D  Btwn  <. A ,  c >.  /\ 
<. D ,  c >.Cgr <. C ,  D >. )  /\  ( C  Btwn  <. A ,  d >.  /\ 
<. C ,  d >.Cgr <. C ,  D >. ) )  /\  ( ( c  Btwn  <. A , 
b >.  /\  <. c ,  b >.Cgr <. C ,  B >. )  /\  ( d 
Btwn  <. A ,  b
>.  /\  <. d ,  b
>.Cgr <. D ,  B >. ) ) )  /\  ( ( E  Btwn  <. C ,  c >.  /\  E  Btwn  <. D , 
d >. )  /\  (
( C  Btwn  <. c ,  P >.  /\  <. C ,  P >.Cgr <. C ,  d
>. )  /\  ( C  Btwn  <. d ,  R >.  /\  <. C ,  R >.Cgr
<. C ,  E >. )  /\  ( R  Btwn  <. P ,  Q >.  /\ 
<. R ,  Q >.Cgr <. R ,  P >. ) ) ) ) )  ->  E  Btwn  <. d ,  D >. )
90 cgrcomlr 24621 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( R  e.  ( EE `  N )  /\  P  e.  ( EE `  N ) )  /\  ( E  e.  ( EE `  N )  /\  d  e.  ( EE `  N ) ) )  ->  ( <. R ,  P >.Cgr <. E ,  d
>. 
<-> 
<. P ,  R >.Cgr <.
d ,  E >. ) )
9122, 23, 24, 86, 25, 90syl122anc 1191 . . . . . . . . 9  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  ( <. R ,  P >.Cgr <. E ,  d >.  <->  <. P ,  R >.Cgr <. d ,  E >. ) )
92 cgrcom 24613 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  R  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  E  e.  ( EE `  N ) ) )  ->  ( <. P ,  R >.Cgr <.
d ,  E >.  <->  <. d ,  E >.Cgr <. P ,  R >. ) )
9322, 24, 23, 25, 86, 92syl122anc 1191 . . . . . . . . 9  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  ( <. P ,  R >.Cgr <.
d ,  E >.  <->  <. d ,  E >.Cgr <. P ,  R >. ) )
9491, 93bitrd 244 . . . . . . . 8  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  ( <. R ,  P >.Cgr <. E ,  d >.  <->  <. d ,  E >.Cgr <. P ,  R >. ) )
9594adantr 451 . . . . . . 7  |-  ( ( ( ( N  e.  NN  /\  A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE
`  N )  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N
) )  /\  (
d  e.  ( EE
`  N )  /\  b  e.  ( EE `  N )  /\  E  e.  ( EE `  N
) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  R  e.  ( EE `  N
) ) )  /\  ( ( ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  c )  /\  ( B  Btwn  <. A ,  C >.  /\  B  Btwn  <. A ,  D >. ) )  /\  ( ( D  Btwn  <. A ,  c >.  /\ 
<. D ,  c >.Cgr <. C ,  D >. )  /\  ( C  Btwn  <. A ,  d >.  /\ 
<. C ,  d >.Cgr <. C ,  D >. ) )  /\  ( ( c  Btwn  <. A , 
b >.  /\  <. c ,  b >.Cgr <. C ,  B >. )  /\  ( d 
Btwn  <. A ,  b
>.  /\  <. d ,  b
>.Cgr <. D ,  B >. ) ) )  /\  ( ( E  Btwn  <. C ,  c >.  /\  E  Btwn  <. D , 
d >. )  /\  (
( C  Btwn  <. c ,  P >.  /\  <. C ,  P >.Cgr <. C ,  d
>. )  /\  ( C  Btwn  <. d ,  R >.  /\  <. C ,  R >.Cgr
<. C ,  E >. )  /\  ( R  Btwn  <. P ,  Q >.  /\ 
<. R ,  Q >.Cgr <. R ,  P >. ) ) ) ) )  ->  ( <. R ,  P >.Cgr <. E ,  d
>. 
<-> 
<. d ,  E >.Cgr <. P ,  R >. ) )
961, 95mpbid 201 . . . . . 6  |-  ( ( ( ( N  e.  NN  /\  A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE
`  N )  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N
) )  /\  (
d  e.  ( EE
`  N )  /\  b  e.  ( EE `  N )  /\  E  e.  ( EE `  N
) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  R  e.  ( EE `  N
) ) )  /\  ( ( ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  c )  /\  ( B  Btwn  <. A ,  C >.  /\  B  Btwn  <. A ,  D >. ) )  /\  ( ( D  Btwn  <. A ,  c >.  /\ 
<. D ,  c >.Cgr <. C ,  D >. )  /\  ( C  Btwn  <. A ,  d >.  /\ 
<. C ,  d >.Cgr <. C ,  D >. ) )  /\  ( ( c  Btwn  <. A , 
b >.  /\  <. c ,  b >.Cgr <. C ,  B >. )  /\  ( d 
Btwn  <. A ,  b
>.  /\  <. d ,  b
>.Cgr <. D ,  B >. ) ) )  /\  ( ( E  Btwn  <. C ,  c >.  /\  E  Btwn  <. D , 
d >. )  /\  (
( C  Btwn  <. c ,  P >.  /\  <. C ,  P >.Cgr <. C ,  d
>. )  /\  ( C  Btwn  <. d ,  R >.  /\  <. C ,  R >.Cgr
<. C ,  E >. )  /\  ( R  Btwn  <. P ,  Q >.  /\ 
<. R ,  Q >.Cgr <. R ,  P >. ) ) ) ) )  ->  <. d ,  E >.Cgr
<. P ,  R >. )
9722, 23, 41, 86, 47, 2cgrcomand 24614 . . . . . 6  |-  ( ( ( ( N  e.  NN  /\  A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE
`  N )  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N
) )  /\  (
d  e.  ( EE
`  N )  /\  b  e.  ( EE `  N )  /\  E  e.  ( EE `  N
) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  R  e.  ( EE `  N
) ) )  /\  ( ( ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  c )  /\  ( B  Btwn  <. A ,  C >.  /\  B  Btwn  <. A ,  D >. ) )  /\  ( ( D  Btwn  <. A ,  c >.  /\ 
<. D ,  c >.Cgr <. C ,  D >. )  /\  ( C  Btwn  <. A ,  d >.  /\ 
<. C ,  d >.Cgr <. C ,  D >. ) )  /\  ( ( c  Btwn  <. A , 
b >.  /\  <. c ,  b >.Cgr <. C ,  B >. )  /\  ( d 
Btwn  <. A ,  b
>.  /\  <. d ,  b
>.Cgr <. D ,  B >. ) ) )  /\  ( ( E  Btwn  <. C ,  c >.  /\  E  Btwn  <. D , 
d >. )  /\  (
( C  Btwn  <. c ,  P >.  /\  <. C ,  P >.Cgr <. C ,  d
>. )  /\  ( C  Btwn  <. d ,  R >.  /\  <. C ,  R >.Cgr
<. C ,  E >. )  /\  ( R  Btwn  <. P ,  Q >.  /\ 
<. R ,  Q >.Cgr <. R ,  P >. ) ) ) ) )  ->  <. E ,  D >.Cgr
<. R ,  Q >. )
98 brcgr3 24669 . . . . . . . 8  |-  ( ( N  e.  NN  /\  ( d  e.  ( EE `  N )  /\  E  e.  ( EE `  N )  /\  D  e.  ( EE `  N ) )  /\  ( P  e.  ( EE `  N )  /\  R  e.  ( EE `  N
)  /\  Q  e.  ( EE `  N ) ) )  ->  ( <. d ,  <. E ,  D >. >.Cgr3 <. P ,  <. R ,  Q >. >.  <->  ( <. d ,  E >.Cgr <. P ,  R >.  /\  <. d ,  D >.Cgr <. P ,  Q >.  /\  <. E ,  D >.Cgr
<. R ,  Q >. ) ) )
9922, 25, 86, 47, 24, 23, 41, 98syl133anc 1205 . . . . . . 7  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  ( <. d ,  <. E ,  D >. >.Cgr3 <. P ,  <. R ,  Q >. >.  <->  ( <. d ,  E >.Cgr <. P ,  R >.  /\  <. d ,  D >.Cgr <. P ,  Q >.  /\  <. E ,  D >.Cgr
<. R ,  Q >. ) ) )
10099adantr 451 . . . . . 6  |-  ( ( ( ( N  e.  NN  /\  A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE
`  N )  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N
) )  /\  (
d  e.  ( EE
`  N )  /\  b  e.  ( EE `  N )  /\  E  e.  ( EE `  N
) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  R  e.  ( EE `  N
) ) )  /\  ( ( ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  c )  /\  ( B  Btwn  <. A ,  C >.  /\  B  Btwn  <. A ,  D >. ) )  /\  ( ( D  Btwn  <. A ,  c >.  /\ 
<. D ,  c >.Cgr <. C ,  D >. )  /\  ( C  Btwn  <. A ,  d >.  /\ 
<. C ,  d >.Cgr <. C ,  D >. ) )  /\  ( ( c  Btwn  <. A , 
b >.  /\  <. c ,  b >.Cgr <. C ,  B >. )  /\  ( d 
Btwn  <. A ,  b
>.  /\  <. d ,  b
>.Cgr <. D ,  B >. ) ) )  /\  ( ( E  Btwn  <. C ,  c >.  /\  E  Btwn  <. D , 
d >. )  /\  (
( C  Btwn  <. c ,  P >.  /\  <. C ,  P >.Cgr <. C ,  d
>. )  /\  ( C  Btwn  <. d ,  R >.  /\  <. C ,  R >.Cgr
<. C ,  E >. )  /\  ( R  Btwn  <. P ,  Q >.  /\ 
<. R ,  Q >.Cgr <. R ,  P >. ) ) ) ) )  ->  ( <. d ,  <. E ,  D >. >.Cgr3 <. P ,  <. R ,  Q >. >.  <->  ( <. d ,  E >.Cgr <. P ,  R >.  /\  <. d ,  D >.Cgr <. P ,  Q >.  /\  <. E ,  D >.Cgr
<. R ,  Q >. ) ) )
10196, 3, 97, 100mpbir3and 1135 . . . . 5  |-  ( ( ( ( N  e.  NN  /\  A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE
`  N )  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N
) )  /\  (
d  e.  ( EE
`  N )  /\  b  e.  ( EE `  N )  /\  E  e.  ( EE `  N
) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  R  e.  ( EE `  N
) ) )  /\  ( ( ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  c )  /\  ( B  Btwn  <. A ,  C >.  /\  B  Btwn  <. A ,  D >. ) )  /\  ( ( D  Btwn  <. A ,  c >.  /\ 
<. D ,  c >.Cgr <. C ,  D >. )  /\  ( C  Btwn  <. A ,  d >.  /\ 
<. C ,  d >.Cgr <. C ,  D >. ) )  /\  ( ( c  Btwn  <. A , 
b >.  /\  <. c ,  b >.Cgr <. C ,  B >. )  /\  ( d 
Btwn  <. A ,  b
>.  /\  <. d ,  b
>.Cgr <. D ,  B >. ) ) )  /\  ( ( E  Btwn  <. C ,  c >.  /\  E  Btwn  <. D , 
d >. )  /\  (
( C  Btwn  <. c ,  P >.  /\  <. C ,  P >.Cgr <. C ,  d
>. )  /\  ( C  Btwn  <. d ,  R >.  /\  <. C ,  R >.Cgr
<. C ,  E >. )  /\  ( R  Btwn  <. P ,  Q >.  /\ 
<. R ,  Q >.Cgr <. R ,  P >. ) ) ) ) )  ->  <. d ,  <. E ,  D >. >.Cgr3 <. P ,  <. R ,  Q >. >.
)
102 simpr1r 1013 . . . . . . . 8  |-  ( ( ( E  Btwn  <. C , 
c >.  /\  E  Btwn  <. D ,  d >. )  /\  ( ( C 
Btwn  <. c ,  P >.  /\  <. C ,  P >.Cgr
<. C ,  d >.
)  /\  ( C  Btwn  <. d ,  R >.  /\  <. C ,  R >.Cgr
<. C ,  E >. )  /\  ( R  Btwn  <. P ,  Q >.  /\ 
<. R ,  Q >.Cgr <. R ,  P >. ) ) )  ->  <. C ,  P >.Cgr <. C ,  d
>. )
103102ad2antll 709 . . . . . . 7  |-  ( ( ( ( N  e.  NN  /\  A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE
`  N )  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N
) )  /\  (
d  e.  ( EE
`  N )  /\  b  e.  ( EE `  N )  /\  E  e.  ( EE `  N
) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  R  e.  ( EE `  N
) ) )  /\  ( ( ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  c )  /\  ( B  Btwn  <. A ,  C >.  /\  B  Btwn  <. A ,  D >. ) )  /\  ( ( D  Btwn  <. A ,  c >.  /\ 
<. D ,  c >.Cgr <. C ,  D >. )  /\  ( C  Btwn  <. A ,  d >.  /\ 
<. C ,  d >.Cgr <. C ,  D >. ) )  /\  ( ( c  Btwn  <. A , 
b >.  /\  <. c ,  b >.Cgr <. C ,  B >. )  /\  ( d 
Btwn  <. A ,  b
>.  /\  <. d ,  b
>.Cgr <. D ,  B >. ) ) )  /\  ( ( E  Btwn  <. C ,  c >.  /\  E  Btwn  <. D , 
d >. )  /\  (
( C  Btwn  <. c ,  P >.  /\  <. C ,  P >.Cgr <. C ,  d
>. )  /\  ( C  Btwn  <. d ,  R >.  /\  <. C ,  R >.Cgr
<. C ,  E >. )  /\  ( R  Btwn  <. P ,  Q >.  /\ 
<. R ,  Q >.Cgr <. R ,  P >. ) ) ) ) )  ->  <. C ,  P >.Cgr
<. C ,  d >.
)
104 cgrcomlr 24621 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( C  e.  ( EE `  N )  /\  P  e.  ( EE `  N ) )  /\  ( C  e.  ( EE `  N )  /\  d  e.  ( EE `  N ) ) )  ->  ( <. C ,  P >.Cgr <. C ,  d
>. 
<-> 
<. P ,  C >.Cgr <.
d ,  C >. ) )
10522, 54, 24, 54, 25, 104syl122anc 1191 . . . . . . . . 9  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  ( <. C ,  P >.Cgr <. C ,  d >.  <->  <. P ,  C >.Cgr <. d ,  C >. ) )
106 cgrcom 24613 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( P  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) ) )  ->  ( <. P ,  C >.Cgr <.
d ,  C >.  <->  <. d ,  C >.Cgr <. P ,  C >. ) )
10722, 24, 54, 25, 54, 106syl122anc 1191 . . . . . . . . 9  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  ( <. P ,  C >.Cgr <.
d ,  C >.  <->  <. d ,  C >.Cgr <. P ,  C >. ) )
108105, 107bitrd 244 . . . . . . . 8  |-  ( ( ( N  e.  NN  /\  A  e.  ( EE
`  N )  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE `  N
)  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N ) )  /\  ( d  e.  ( EE `  N )  /\  b  e.  ( EE `  N
)  /\  E  e.  ( EE `  N ) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N
)  /\  R  e.  ( EE `  N ) ) )  ->  ( <. C ,  P >.Cgr <. C ,  d >.  <->  <. d ,  C >.Cgr <. P ,  C >. ) )
109108adantr 451 . . . . . . 7  |-  ( ( ( ( N  e.  NN  /\  A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE
`  N )  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N
) )  /\  (
d  e.  ( EE
`  N )  /\  b  e.  ( EE `  N )  /\  E  e.  ( EE `  N
) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  R  e.  ( EE `  N
) ) )  /\  ( ( ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  c )  /\  ( B  Btwn  <. A ,  C >.  /\  B  Btwn  <. A ,  D >. ) )  /\  ( ( D  Btwn  <. A ,  c >.  /\ 
<. D ,  c >.Cgr <. C ,  D >. )  /\  ( C  Btwn  <. A ,  d >.  /\ 
<. C ,  d >.Cgr <. C ,  D >. ) )  /\  ( ( c  Btwn  <. A , 
b >.  /\  <. c ,  b >.Cgr <. C ,  B >. )  /\  ( d 
Btwn  <. A ,  b
>.  /\  <. d ,  b
>.Cgr <. D ,  B >. ) ) )  /\  ( ( E  Btwn  <. C ,  c >.  /\  E  Btwn  <. D , 
d >. )  /\  (
( C  Btwn  <. c ,  P >.  /\  <. C ,  P >.Cgr <. C ,  d
>. )  /\  ( C  Btwn  <. d ,  R >.  /\  <. C ,  R >.Cgr
<. C ,  E >. )  /\  ( R  Btwn  <. P ,  Q >.  /\ 
<. R ,  Q >.Cgr <. R ,  P >. ) ) ) ) )  ->  ( <. C ,  P >.Cgr <. C ,  d
>. 
<-> 
<. d ,  C >.Cgr <. P ,  C >. ) )
110103, 109mpbid 201 . . . . . 6  |-  ( ( ( ( N  e.  NN  /\  A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE
`  N )  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N
) )  /\  (
d  e.  ( EE
`  N )  /\  b  e.  ( EE `  N )  /\  E  e.  ( EE `  N
) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  R  e.  ( EE `  N
) ) )  /\  ( ( ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  c )  /\  ( B  Btwn  <. A ,  C >.  /\  B  Btwn  <. A ,  D >. ) )  /\  ( ( D  Btwn  <. A ,  c >.  /\ 
<. D ,  c >.Cgr <. C ,  D >. )  /\  ( C  Btwn  <. A ,  d >.  /\ 
<. C ,  d >.Cgr <. C ,  D >. ) )  /\  ( ( c  Btwn  <. A , 
b >.  /\  <. c ,  b >.Cgr <. C ,  B >. )  /\  ( d 
Btwn  <. A ,  b
>.  /\  <. d ,  b
>.Cgr <. D ,  B >. ) ) )  /\  ( ( E  Btwn  <. C ,  c >.  /\  E  Btwn  <. D , 
d >. )  /\  (
( C  Btwn  <. c ,  P >.  /\  <. C ,  P >.Cgr <. C ,  d
>. )  /\  ( C  Btwn  <. d ,  R >.  /\  <. C ,  R >.Cgr
<. C ,  E >. )  /\  ( R  Btwn  <. P ,  Q >.  /\ 
<. R ,  Q >.Cgr <. R ,  P >. ) ) ) ) )  ->  <. d ,  C >.Cgr
<. P ,  C >. )
1118ad2antll 709 . . . . . . 7  |-  ( ( ( ( N  e.  NN  /\  A  e.  ( EE `  N
)  /\  B  e.  ( EE `  N ) )  /\  ( ( C  e.  ( EE
`  N )  /\  D  e.  ( EE `  N )  /\  c  e.  ( EE `  N
) )  /\  (
d  e.  ( EE
`  N )  /\  b  e.  ( EE `  N )  /\  E  e.  ( EE `  N
) ) )  /\  ( P  e.  ( EE `  N )  /\  Q  e.  ( EE `  N )  /\  R  e.  ( EE `  N
) ) )  /\  ( ( ( ( A  =/=  B  /\  B  =/=  C  /\  C  =/=  c )  /\  ( B  Btwn  <. A ,  C >.  /\  B  Btwn  <. A ,  D >. ) )  /\  ( ( D  Btwn  <. A ,  c >.  /\ 
<. D ,  c >.Cgr <. C ,  D >. )  /\  ( C  Btwn  <. A ,  d >.  /\ 
<. C ,  d >.Cgr <. C ,  D >. ) )  /\  ( ( c  Btwn  <. A , 
b >.  /\  <. c ,  b >.Cgr <. C ,  B >. )  /\  ( d 
Btwn  <. A ,  b
>.  /\  <. d ,  b
>.Cgr <. D ,  B >. ) ) )  /\  ( ( E  Btwn  <. C ,  c >.  /\  E  Btwn  <. D , 
d >. )  /\  (
( C  Btwn  <. c ,  P >.  /\  <. C ,  P >.Cgr <. C ,  d
>. )  /\  ( C  Btwn  <. d ,  R >.  /\  <. C ,  R >.Cgr
<. C ,  E >. )  /\  ( R  Btwn  <. P ,  Q >.  /\ 
<. R ,  Q >.Cgr <. R ,  P >. ) ) ) ) )  ->  <. C ,  R >.Cgr
<. C ,  E >. )
112 cgrcomlr 24621 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( C  e.  ( EE `  N )  /\  R  e.  ( EE `  N ) )  /\  ( C  e.  ( EE `  N )  /\  E  e.