Metamath Proof Explorer


Theorem btwnconn1lem12

Description: Lemma for btwnconn1 . Using a long string of invocations of linecgr , we show that D = d . (Contributed by Scott Fenton, 9-Oct-2013)

Ref Expression
Assertion btwnconn1lem12
|- ( ( ( ( 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 )

Proof

Step Hyp Ref Expression
1 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 )
2 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 ) )
3 simp2l3
 |-  ( ( ( 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 ) )
4 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 ) )
5 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 ) )
6 simp1l3
 |-  ( ( ( ( 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 >. ) ) ) -> C =/= c )
7 6 ad2antrl
 |-  ( ( ( ( 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 =/= c )
8 simpr1l
 |-  ( ( ( 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 Btwn <. c , P >. )
9 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 Btwn <. c , P >. )
10 btwncolinear5
 |-  ( ( N e. NN /\ ( c e. ( EE ` N ) /\ P e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( C Btwn <. c , P >. -> C Colinear <. c , P >. ) )
11 1 3 4 2 10 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 ) ) ) -> ( C Btwn <. c , P >. -> C Colinear <. c , P >. ) )
12 11 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 Btwn <. c , P >. -> C Colinear <. c , P >. ) )
13 9 12 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 >. ) ) ) ) ) -> C Colinear <. c , P >. )
14 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 ) )
15 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 ) )
16 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 >. )
17 16 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 >. )
18 simp2rr
 |-  ( ( ( ( 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 >. ) ) ) -> <. C , d >. Cgr <. C , D >. )
19 18 ad2antrl
 |-  ( ( ( ( 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 , d >. Cgr <. C , D >. )
20 1 2 4 2 15 2 14 17 19 cgrtrand
 |-  ( ( ( ( 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 >. )
21 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 >. )
22 1 14 2 5 2 21 cgrcomlrand
 |-  ( ( ( ( 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 , D >. Cgr <. C , Q >. )
23 1 2 4 2 14 2 5 20 22 cgrtrand
 |-  ( ( ( ( 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 , Q >. )
24 simp12
 |-  ( ( ( 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 e. ( EE ` N ) )
25 simp13
 |-  ( ( ( 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 ) ) ) -> B e. ( EE ` N ) )
26 simp2r2
 |-  ( ( ( 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 ) ) ) -> b e. ( EE ` N ) )
27 simp1rr
 |-  ( ( ( ( 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 >. ) ) ) -> B Btwn <. A , D >. )
28 27 ad2antrl
 |-  ( ( ( ( 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 >. ) ) ) ) ) -> B Btwn <. A , D >. )
29 simp2ll
 |-  ( ( ( ( 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 >. ) ) ) -> D Btwn <. A , c >. )
30 29 ad2antrl
 |-  ( ( ( ( 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 Btwn <. A , c >. )
31 1 24 25 14 3 28 30 btwnexchand
 |-  ( ( ( ( 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 >. ) ) ) ) ) -> B Btwn <. A , c >. )
32 simp3ll
 |-  ( ( ( ( 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 >. ) ) ) -> c Btwn <. A , b >. )
33 32 ad2antrl
 |-  ( ( ( ( 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 Btwn <. A , b >. )
34 1 24 25 3 26 31 33 btwnexch3and
 |-  ( ( ( ( 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 Btwn <. B , b >. )
35 opeq1
 |-  ( B = b -> <. B , b >. = <. b , b >. )
36 35 breq2d
 |-  ( B = b -> ( c Btwn <. B , b >. <-> c Btwn <. b , b >. ) )
37 36 biimpac
 |-  ( ( c Btwn <. B , b >. /\ B = b ) -> c Btwn <. b , b >. )
38 axbtwnid
 |-  ( ( N e. NN /\ c e. ( EE ` N ) /\ b e. ( EE ` N ) ) -> ( c Btwn <. b , b >. -> c = b ) )
39 1 3 26 38 syl3anc
 |-  ( ( ( 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 Btwn <. b , b >. -> c = b ) )
40 37 39 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 ) ) ) -> ( ( c Btwn <. B , b >. /\ B = b ) -> c = b ) )
41 40 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 ) ) ) -> ( c Btwn <. B , b >. -> ( B = b -> c = b ) ) )
42 41 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 Btwn <. B , b >. -> ( B = b -> c = b ) ) )
43 34 42 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 >. ) ) ) ) ) -> ( B = b -> c = b ) )
44 simp1
 |-  ( ( ( 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 /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) )
45 simp2l
 |-  ( ( ( 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 ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) )
46 simp2r
 |-  ( ( ( 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 ) /\ b e. ( EE ` N ) /\ E e. ( EE ` N ) ) )
47 44 45 46 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 ) ) ) -> ( ( 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 ) ) ) )
48 simpl
 |-  ( ( ( ( ( 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 >. ) ) ) ) -> ( ( ( 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 >. ) ) ) )
49 simprl
 |-  ( ( ( ( ( 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 <. C , c >. /\ E Btwn <. D , d >. ) )
50 48 49 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 >. ) ) ) ) -> ( ( ( ( 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 >. ) ) )
51 btwnconn1lem7
 |-  ( ( ( ( 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 ) ) ) /\ ( ( ( ( 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 =/= d )
52 47 50 51 syl2an
 |-  ( ( ( ( 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 =/= d )
53 simp2rl
 |-  ( ( ( ( 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 >. ) ) ) -> C Btwn <. A , d >. )
54 53 ad2antrl
 |-  ( ( ( ( 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 Btwn <. A , d >. )
55 simp3rl
 |-  ( ( ( ( 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 >. ) ) ) -> d Btwn <. A , b >. )
56 55 ad2antrl
 |-  ( ( ( ( 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 Btwn <. A , b >. )
57 1 24 2 15 26 54 56 btwnexch3and
 |-  ( ( ( ( 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 Btwn <. C , b >. )
58 btwncolinear2
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ b e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) -> ( d Btwn <. C , b >. -> C Colinear <. d , b >. ) )
59 1 2 26 15 58 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 Btwn <. C , b >. -> C Colinear <. d , b >. ) )
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 ) ) ) /\ ( ( ( ( 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 Btwn <. C , b >. -> C Colinear <. d , b >. ) )
61 57 60 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 >. ) ) ) ) ) -> C Colinear <. d , b >. )
62 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 ) )
63 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 >. )
64 63 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 >. )
65 btwnconn1lem5
 |-  ( ( ( ( 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 ) ) ) /\ ( ( ( ( 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 >. ) ) ) -> <. E , C >. Cgr <. E , c >. )
66 47 50 65 syl2an
 |-  ( ( ( ( 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 <. E , c >. )
67 opeq2
 |-  ( R = C -> <. C , R >. = <. C , C >. )
68 67 breq1d
 |-  ( R = C -> ( <. C , R >. Cgr <. C , E >. <-> <. C , C >. Cgr <. C , E >. ) )
69 68 anbi1d
 |-  ( R = C -> ( ( <. C , R >. Cgr <. C , E >. /\ <. E , C >. Cgr <. E , c >. ) <-> ( <. C , C >. Cgr <. C , E >. /\ <. E , C >. Cgr <. E , c >. ) ) )
70 69 biimpac
 |-  ( ( ( <. C , R >. Cgr <. C , E >. /\ <. E , C >. Cgr <. E , c >. ) /\ R = C ) -> ( <. C , C >. Cgr <. C , E >. /\ <. E , C >. Cgr <. E , c >. ) )
71 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 ) )
72 cgrid2
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ C e. ( EE ` N ) /\ E e. ( EE ` N ) ) ) -> ( <. C , C >. Cgr <. C , E >. -> C = E ) )
73 1 2 2 71 72 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 ) ) ) -> ( <. C , C >. Cgr <. C , E >. -> C = E ) )
74 opeq1
 |-  ( C = E -> <. C , C >. = <. E , C >. )
75 opeq1
 |-  ( C = E -> <. C , c >. = <. E , c >. )
76 74 75 breq12d
 |-  ( C = E -> ( <. C , C >. Cgr <. C , c >. <-> <. E , C >. Cgr <. E , c >. ) )
77 76 biimpar
 |-  ( ( C = E /\ <. E , C >. Cgr <. E , c >. ) -> <. C , C >. Cgr <. C , c >. )
78 cgrid2
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ C e. ( EE ` N ) /\ c e. ( EE ` N ) ) ) -> ( <. C , C >. Cgr <. C , c >. -> C = c ) )
79 1 2 2 3 78 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 ) ) ) -> ( <. C , C >. Cgr <. C , c >. -> C = c ) )
80 77 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 ) ) ) -> ( ( C = E /\ <. E , C >. Cgr <. E , c >. ) -> C = c ) )
81 73 80 syland
 |-  ( ( ( 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 , C >. Cgr <. C , E >. /\ <. E , C >. Cgr <. E , c >. ) -> C = c ) )
82 70 81 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 ) ) ) -> ( ( ( <. C , R >. Cgr <. C , E >. /\ <. E , C >. Cgr <. E , c >. ) /\ R = C ) -> C = c ) )
83 82 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 ) ) ) -> ( ( <. C , R >. Cgr <. C , E >. /\ <. E , C >. Cgr <. E , c >. ) -> ( R = C -> C = c ) ) )
84 83 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 <. E , c >. ) -> ( R = C -> C = c ) ) )
85 64 66 84 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 >. ) ) ) ) ) -> ( R = C -> C = c ) )
86 85 necon3d
 |-  ( ( ( ( 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 =/= c -> R =/= C ) )
87 7 86 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 >. ) ) ) ) ) -> R =/= C )
88 simpr2l
 |-  ( ( ( 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 Btwn <. d , R >. )
89 88 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 Btwn <. d , R >. )
90 btwncolinear4
 |-  ( ( N e. NN /\ ( d e. ( EE ` N ) /\ R e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( C Btwn <. d , R >. -> R Colinear <. C , d >. ) )
91 1 15 62 2 90 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 ) ) ) -> ( C Btwn <. d , R >. -> R Colinear <. C , d >. ) )
92 91 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 Btwn <. d , R >. -> R Colinear <. C , d >. ) )
93 89 92 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 >. ) ) ) ) ) -> R Colinear <. C , d >. )
94 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 >. )
95 94 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 >. ) ) ) ) ) -> <. R , Q >. Cgr <. R , P >. )
96 1 62 5 62 4 95 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 >. ) ) ) ) ) -> <. R , P >. Cgr <. R , Q >. )
97 1 62 2 15 4 5 87 93 96 23 linecgrand
 |-  ( ( ( ( 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 , P >. Cgr <. d , Q >. )
98 1 2 15 26 4 5 52 61 23 97 linecgrand
 |-  ( ( ( ( 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 >. ) ) ) ) ) -> <. b , P >. Cgr <. b , Q >. )
99 opeq1
 |-  ( c = b -> <. c , P >. = <. b , P >. )
100 opeq1
 |-  ( c = b -> <. c , Q >. = <. b , Q >. )
101 99 100 breq12d
 |-  ( c = b -> ( <. c , P >. Cgr <. c , Q >. <-> <. b , P >. Cgr <. b , Q >. ) )
102 101 biimprd
 |-  ( c = b -> ( <. b , P >. Cgr <. b , Q >. -> <. c , P >. Cgr <. c , Q >. ) )
103 43 98 102 syl6ci
 |-  ( ( ( ( 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 >. ) ) ) ) ) -> ( B = b -> <. c , P >. Cgr <. c , Q >. ) )
104 103 com12
 |-  ( B = b -> ( ( ( ( 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 , Q >. ) )
105 simprl
 |-  ( ( ( ( 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 ) ) ) /\ ( B =/= b /\ ( ( ( ( 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 >. ) ) ) ) ) ) -> B =/= b )
106 34 adantrl
 |-  ( ( ( ( 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 ) ) ) /\ ( B =/= b /\ ( ( ( ( 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 Btwn <. B , b >. )
107 btwncolinear1
 |-  ( ( N e. NN /\ ( B e. ( EE ` N ) /\ b e. ( EE ` N ) /\ c e. ( EE ` N ) ) ) -> ( c Btwn <. B , b >. -> B Colinear <. b , c >. ) )
108 1 25 26 3 107 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 ) ) ) -> ( c Btwn <. B , b >. -> B Colinear <. b , 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 ) ) ) /\ ( B =/= b /\ ( ( ( ( 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 Btwn <. B , b >. -> B Colinear <. b , c >. ) )
110 106 109 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 ) ) ) /\ ( B =/= b /\ ( ( ( ( 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 >. ) ) ) ) ) ) -> B Colinear <. b , c >. )
111 simp1rl
 |-  ( ( ( ( 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 >. ) ) ) -> B Btwn <. A , C >. )
112 111 ad2antrl
 |-  ( ( ( ( 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 >. ) ) ) ) ) -> B Btwn <. A , C >. )
113 1 24 25 2 15 112 54 btwnexch3and
 |-  ( ( ( ( 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 Btwn <. B , d >. )
114 btwncolinear6
 |-  ( ( N e. NN /\ ( B e. ( EE ` N ) /\ d e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( C Btwn <. B , d >. -> C Colinear <. d , B >. ) )
115 1 25 15 2 114 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 ) ) ) -> ( C Btwn <. B , d >. -> C Colinear <. d , B >. ) )
116 115 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 Btwn <. B , d >. -> C Colinear <. d , B >. ) )
117 113 116 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 >. ) ) ) ) ) -> C Colinear <. d , B >. )
118 1 2 15 25 4 5 52 117 23 97 linecgrand
 |-  ( ( ( ( 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 >. ) ) ) ) ) -> <. B , P >. Cgr <. B , Q >. )
119 118 adantrl
 |-  ( ( ( ( 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 ) ) ) /\ ( B =/= b /\ ( ( ( ( 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 >. ) ) ) ) ) ) -> <. B , P >. Cgr <. B , Q >. )
120 98 adantrl
 |-  ( ( ( ( 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 ) ) ) /\ ( B =/= b /\ ( ( ( ( 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 >. ) ) ) ) ) ) -> <. b , P >. Cgr <. b , Q >. )
121 1 25 26 3 4 5 105 110 119 120 linecgrand
 |-  ( ( ( ( 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 ) ) ) /\ ( B =/= b /\ ( ( ( ( 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 , Q >. )
122 121 an12s
 |-  ( ( B =/= b /\ ( ( ( 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 , Q >. )
123 122 ex
 |-  ( B =/= b -> ( ( ( ( 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 , Q >. ) )
124 104 123 pm2.61ine
 |-  ( ( ( ( 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 , Q >. )
125 1 2 3 4 4 5 7 13 23 124 linecgrand
 |-  ( ( ( ( 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 >. ) ) ) ) ) -> <. P , P >. Cgr <. P , Q >. )
126 cgrid2
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ P e. ( EE ` N ) /\ Q e. ( EE ` N ) ) ) -> ( <. P , P >. Cgr <. P , Q >. -> P = Q ) )
127 1 4 4 5 126 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 , P >. Cgr <. P , Q >. -> P = Q ) )
128 127 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 >. ) ) ) ) ) -> ( <. P , P >. Cgr <. P , Q >. -> P = Q ) )
129 125 128 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 >. ) ) ) ) ) -> P = Q )
130 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 >. )
131 opeq1
 |-  ( P = Q -> <. P , Q >. = <. Q , Q >. )
132 131 breq2d
 |-  ( P = Q -> ( <. d , D >. Cgr <. P , Q >. <-> <. d , D >. Cgr <. Q , Q >. ) )
133 132 biimpa
 |-  ( ( P = Q /\ <. d , D >. Cgr <. P , Q >. ) -> <. d , D >. Cgr <. Q , Q >. )
134 axcgrid
 |-  ( ( N e. NN /\ ( d e. ( EE ` N ) /\ D e. ( EE ` N ) /\ Q e. ( EE ` N ) ) ) -> ( <. d , D >. Cgr <. Q , Q >. -> d = D ) )
135 1 15 14 5 134 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 <. Q , Q >. -> d = D ) )
136 133 135 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 /\ <. d , D >. Cgr <. P , Q >. ) -> d = D ) )
137 136 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 >. ) ) ) ) ) -> ( ( P = Q /\ <. d , D >. Cgr <. P , Q >. ) -> d = D ) )
138 129 130 137 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 = D )
139 138 eqcomd
 |-  ( ( ( ( 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 )