Theorem btwnconn1lem11

Description: Lemma for btwnconn1 . Now, we establish that D and Q are equidistant from C . (Contributed by Scott Fenton, 8-Oct-2013)

	Ref	Expression
Assertion	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

Step	Hyp	Ref	Expression
1		btwnconn1lem8	|- ( ( ( ( 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	|- ( ( ( ( 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	|- ( ( ( ( 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 >. )
4	1 2 3	3jca	|- ( ( ( ( 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 >. ) )
5	4	adantr	|- ( ( ( ( ( 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	|- ( ( ( 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 >. )
7	6	adantl	|- ( ( ( ( ( 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	|- ( ( ( 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 >. )
9	8	adantl	|- ( ( ( ( ( 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 >. )
10	7 9	jca	|- ( ( ( ( ( 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	|- ( d = E -> <. C , d >. = <. C , E >. )
12	11	breq2d	|- ( d = E -> ( <. C , R >. Cgr <. C , d >. <-> <. C , R >. Cgr <. C , E >. ) )
13	12	anbi2d	|- ( d = E -> ( ( <. R , Q >. Cgr <. R , P >. /\ <. C , R >. Cgr <. C , d >. ) <-> ( <. R , Q >. Cgr <. R , P >. /\ <. C , R >. Cgr <. C , E >. ) ) )
14		opeq1	|- ( d = E -> <. d , d >. = <. E , d >. )
15	14	breq2d	|- ( d = E -> ( <. R , P >. Cgr <. d , d >. <-> <. R , P >. Cgr <. E , d >. ) )
16		opeq1	|- ( d = E -> <. d , D >. = <. E , D >. )
17	16	breq2d	|- ( d = E -> ( <. R , Q >. Cgr <. d , D >. <-> <. R , Q >. Cgr <. E , D >. ) )
18	15 17	3anbi12d	|- ( 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 >. ) ) )
19	13 18	anbi12d	|- ( 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 >. ) ) ) )
20	19	biimpar	|- ( ( 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	|- ( ( ( <. 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	|- ( ( ( 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	|- ( ( ( 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	|- ( ( ( 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	|- ( ( ( 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	|- ( ( N e. NN /\ ( R e. ( EE ` N ) /\ P e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) -> ( <. R , P >. Cgr <. d , d >. -> R = P ) )
27	22 23 24 25 26	syl13anc	|- ( ( ( 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 ) )
28	21 27	syl5	|- ( ( ( 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	|- ( R = P -> <. R , Q >. = <. P , Q >. )
30		opeq1	|- ( R = P -> <. R , P >. = <. P , P >. )
31	29 30	breq12d	|- ( R = P -> ( <. R , Q >. Cgr <. R , P >. <-> <. P , Q >. Cgr <. P , P >. ) )
32		opeq2	|- ( R = P -> <. C , R >. = <. C , P >. )
33	32	breq1d	|- ( R = P -> ( <. C , R >. Cgr <. C , d >. <-> <. C , P >. Cgr <. C , d >. ) )
34	31 33	anbi12d	|- ( R = P -> ( ( <. R , Q >. Cgr <. R , P >. /\ <. C , R >. Cgr <. C , d >. ) <-> ( <. P , Q >. Cgr <. P , P >. /\ <. C , P >. Cgr <. C , d >. ) ) )
35	30	breq1d	|- ( R = P -> ( <. R , P >. Cgr <. d , d >. <-> <. P , P >. Cgr <. d , d >. ) )
36	29	breq1d	|- ( R = P -> ( <. R , Q >. Cgr <. d , D >. <-> <. P , Q >. Cgr <. d , D >. ) )
37	35 36	3anbi12d	|- ( 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 >. ) ) )
38	34 37	anbi12d	|- ( 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 >. ) ) ) )
39	38	biimpac	|- ( ( ( ( <. 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	|- ( ( ( <. 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	|- ( ( ( 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	|- ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( <. P , Q >. Cgr <. P , P >. -> P = Q ) )
43	22 24 41 24 42	syl13anc	|- ( ( ( 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 ) )
44	40 43	syl5	|- ( ( ( 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	|- ( ( ( ( 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	|- ( ( ( <. 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	|- ( ( ( 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	|- ( ( N e. NN /\ ( d e. ( EE ` N ) /\ D e. ( EE ` N ) /\ P e. ( EE ` N ) ) ) -> ( <. d , D >. Cgr <. P , P >. -> d = D ) )
49	22 25 47 24 48	syl13anc	|- ( ( ( 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 ) )
50	46 49	syl5	|- ( ( ( 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 ) )
51	50	imp	|- ( ( ( ( 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 )
52	51	opeq2d	|- ( ( ( ( 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 >. )
53	52	breq2d	|- ( ( ( ( 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	|- ( ( ( 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	|- ( ( 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 >. ) )
56	22 54 24 54 47 55	syl122anc	|- ( ( ( 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	|- ( ( 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 >. ) )
58	22 24 54 47 54 57	syl122anc	|- ( ( ( 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 >. ) )
59	56 58	bitrd	|- ( ( ( 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 >. ) )
60	59	adantr	|- ( ( ( ( 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 >. ) )
61	53 60	bitrd	|- ( ( ( ( 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 >. ) )
62	45 61	mpbid	|- ( ( ( ( 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 >. )
63	62	ex	|- ( ( ( 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	|- ( P = Q -> <. P , P >. = <. P , Q >. )
65	64	breq1d	|- ( P = Q -> ( <. P , P >. Cgr <. P , P >. <-> <. P , Q >. Cgr <. P , P >. ) )
66	65	anbi1d	|- ( P = Q -> ( ( <. P , P >. Cgr <. P , P >. /\ <. C , P >. Cgr <. C , d >. ) <-> ( <. P , Q >. Cgr <. P , P >. /\ <. C , P >. Cgr <. C , d >. ) ) )
67	64	breq1d	|- ( P = Q -> ( <. P , P >. Cgr <. d , D >. <-> <. P , Q >. Cgr <. d , D >. ) )
68	64	breq2d	|- ( P = Q -> ( <. d , D >. Cgr <. P , P >. <-> <. d , D >. Cgr <. P , Q >. ) )
69	67 68	3anbi23d	|- ( 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 >. ) ) )
70	66 69	anbi12d	|- ( 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	|- ( P = Q -> <. P , C >. = <. Q , C >. )
72	71	breq2d	|- ( P = Q -> ( <. D , C >. Cgr <. P , C >. <-> <. D , C >. Cgr <. Q , C >. ) )
73	70 72	imbi12d	|- ( 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 >. ) ) )
74	63 73	syl5ibcom	|- ( ( ( 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 >. ) ) )
75	74	com23	|- ( ( ( 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 >. ) ) )
76	44 75	mpdd	|- ( ( ( 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 >. ) )
77	39 76	syl5	|- ( ( ( 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 >. ) )
78	77	expd	|- ( ( ( 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 >. ) ) )
79	28 78	mpdd	|- ( ( ( 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 >. ) )
80	20 79	syl5	|- ( ( ( 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 >. ) )
81	80	exp4d	|- ( ( ( 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 >. ) ) ) )
82	81	com23	|- ( ( ( 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 >. ) ) ) )
83	10 82	syl5	|- ( ( ( 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 >. ) ) ) )
84	83	imp31	|- ( ( ( ( ( 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 >. ) )
85	5 84	mpd	|- ( ( ( ( ( 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	|- ( ( ( 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	|- ( ( ( ( ( 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 >. )
88	87	adantl	|- ( ( ( ( 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 >. )
89	22 86 47 25 88	btwncomand	|- ( ( ( ( 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	|- ( ( 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 >. ) )
91	22 23 24 86 25 90	syl122anc	|- ( ( ( 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	|- ( ( 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 >. ) )
93	22 24 23 25 86 92	syl122anc	|- ( ( ( 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 >. ) )
94	91 93	bitrd	|- ( ( ( 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 >. ) )
95	94	adantr	|- ( ( ( ( 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 >. ) )
96	1 95	mpbid	|- ( ( ( ( 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 >. )
97	22 23 41 86 47 2	cgrcomand	|- ( ( ( ( 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	|- ( ( 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 >. ) ) )
99	22 25 86 47 24 23 41 98	syl133anc	|- ( ( ( 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 >. ) ) )
100	99	adantr	|- ( ( ( ( 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 >. ) ) )
101	96 3 97 100	mpbir3and	|- ( ( ( ( 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	|- ( ( ( 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 >. )
103	102	ad2antll	|- ( ( ( ( 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	|- ( ( 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 >. ) )
105	22 54 24 54 25 104	syl122anc	|- ( ( ( 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	|- ( ( 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 >. ) )
107	22 24 54 25 54 106	syl122anc	|- ( ( ( 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 >. ) )
108	105 107	bitrd	|- ( ( ( 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 >. ) )
109	108	adantr	|- ( ( ( ( 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 >. ) )
110	103 109	mpbid	|- ( ( ( ( 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 >. )
111	8	ad2antll	|- ( ( ( ( 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	|- ( ( N e. NN /\ ( C e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( <. C , R >. Cgr <. C , E >. <-> <. R , C >. Cgr <. E , C >. ) )
113	22 54 23 54 86 112	syl122anc	|- ( ( ( 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 , R >. Cgr <. C , E >. <-> <. R , C >. Cgr <. E , C >. ) )
114		cgrcom	|- ( ( N e. NN /\ ( R e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. R , C >. Cgr <. E , C >. <-> <. E , C >. Cgr <. R , C >. ) )
115	22 23 54 86 54 114	syl122anc	|- ( ( ( 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 , C >. Cgr <. E , C >. <-> <. E , C >. Cgr <. R , C >. ) )
116	113 115	bitrd	|- ( ( ( 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 , R >. Cgr <. C , E >. <-> <. E , C >. Cgr <. R , C >. ) )
117	116	adantr	|- ( ( ( ( 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 >. <-> <. E , C >. Cgr <. R , C >. ) )
118	111 117	mpbid	|- ( ( ( ( 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 , C >. Cgr <. R , C >. )
119	110 118	jca	|- ( ( ( ( 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 >. /\ <. E , C >. Cgr <. R , C >. ) )
120	89 101 119	3jca	|- ( ( ( ( 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 >. /\ <. d , <. E , D >. >. Cgr3 <. P , <. R , Q >. >. /\ ( <. d , C >. Cgr <. P , C >. /\ <. E , C >. Cgr <. R , C >. ) ) )
121	120	adantr	|- ( ( ( ( ( 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 ) -> ( E Btwn <. d , D >. /\ <. d , <. E , D >. >. Cgr3 <. P , <. R , Q >. >. /\ ( <. d , C >. Cgr <. P , C >. /\ <. E , C >. Cgr <. R , C >. ) ) )
122		simpr	|- ( ( ( ( ( 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 =/= E )
123		brofs2	|- ( ( ( N e. NN /\ d e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ C e. ( EE ` N ) /\ P e. ( EE ` N ) ) /\ ( R e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. <. d , E >. , <. D , C >. >. OuterFiveSeg <. <. P , R >. , <. Q , C >. >. <-> ( E Btwn <. d , D >. /\ <. d , <. E , D >. >. Cgr3 <. P , <. R , Q >. >. /\ ( <. d , C >. Cgr <. P , C >. /\ <. E , C >. Cgr <. R , C >. ) ) ) )
124	123	anbi1d	|- ( ( ( N e. NN /\ d e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ C e. ( EE ` N ) /\ P e. ( EE ` N ) ) /\ ( R e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( <. <. d , E >. , <. D , C >. >. OuterFiveSeg <. <. P , R >. , <. Q , C >. >. /\ d =/= E ) <-> ( ( E Btwn <. d , D >. /\ <. d , <. E , D >. >. Cgr3 <. P , <. R , Q >. >. /\ ( <. d , C >. Cgr <. P , C >. /\ <. E , C >. Cgr <. R , C >. ) ) /\ d =/= E ) ) )
125		5segofs	|- ( ( ( N e. NN /\ d e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ C e. ( EE ` N ) /\ P e. ( EE ` N ) ) /\ ( R e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( <. <. d , E >. , <. D , C >. >. OuterFiveSeg <. <. P , R >. , <. Q , C >. >. /\ d =/= E ) -> <. D , C >. Cgr <. Q , C >. ) )
126	124 125	sylbird	|- ( ( ( N e. NN /\ d e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ C e. ( EE ` N ) /\ P e. ( EE ` N ) ) /\ ( R e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( ( E Btwn <. d , D >. /\ <. d , <. E , D >. >. Cgr3 <. P , <. R , Q >. >. /\ ( <. d , C >. Cgr <. P , C >. /\ <. E , C >. Cgr <. R , C >. ) ) /\ d =/= E ) -> <. D , C >. Cgr <. Q , C >. ) )
127	22 25 86 47 54 24 23 41 54 126	syl333anc	|- ( ( ( 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 Btwn <. d , D >. /\ <. d , <. E , D >. >. Cgr3 <. P , <. R , Q >. >. /\ ( <. d , C >. Cgr <. P , C >. /\ <. E , C >. Cgr <. R , C >. ) ) /\ d =/= E ) -> <. D , C >. Cgr <. Q , C >. ) )
128	127	ad2antrr	|- ( ( ( ( ( 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 ) -> ( ( ( E Btwn <. d , D >. /\ <. d , <. E , D >. >. Cgr3 <. P , <. R , Q >. >. /\ ( <. d , C >. Cgr <. P , C >. /\ <. E , C >. Cgr <. R , C >. ) ) /\ d =/= E ) -> <. D , C >. Cgr <. Q , C >. ) )
129	121 122 128	mp2and	|- ( ( ( ( ( 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 >. )
130	85 129	pm2.61dane	|- ( ( ( ( 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 >. )