Metamath Proof Explorer

Theorem btwnconn1lem13

Description: Lemma for btwnconn1 . Begin back-filling and eliminating hypotheses. (Contributed by Scott Fenton, 9-Oct-2013)

Ref Expression
Assertion btwnconn1lem13 
|- ( ( ( ( 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 ) ) ) ) /\ ( ( ( A =/= B /\ B =/= 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 \/ D = d ) )

Proof

Step Hyp Ref Expression
1 df-ne 
 |-  ( C =/= c <-> -. C = c )
2 simp2rl 
 |-  ( ( ( ( A =/= B /\ B =/= 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 >. )
3 2 adantr 
 |-  ( ( ( ( ( A =/= B /\ B =/= 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 ) -> C Btwn <. A , d >. )
4 simp2ll 
 |-  ( ( ( ( A =/= B /\ B =/= 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 >. )
5 4 adantr 
 |-  ( ( ( ( ( A =/= B /\ B =/= 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 ) -> D Btwn <. A , c >. )
6 3 5 jca 
 |-  ( ( ( ( ( A =/= B /\ B =/= 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 ) -> ( C Btwn <. A , d >. /\ D Btwn <. A , c >. ) )
7 simpl1 
 |-  ( ( ( 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 ) ) ) ) -> N e. NN )
8 simprl1 
 |-  ( ( ( 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 ) ) ) ) -> C e. ( EE ` N ) )
9 simpl2 
 |-  ( ( ( 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 ) ) ) ) -> A e. ( EE ` N ) )
10 simprrl 
 |-  ( ( ( 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 ) ) ) ) -> d e. ( EE ` N ) )
11 btwncom 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ A e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) -> ( C Btwn <. A , d >. <-> C Btwn <. d , A >. ) )
12 7 8 9 10 11 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 ) ) ) ) -> ( C Btwn <. A , d >. <-> C Btwn <. d , A >. ) )
13 simprl2 
 |-  ( ( ( 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 ) ) ) ) -> D e. ( EE ` N ) )
14 simprl3 
 |-  ( ( ( 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 ) ) ) ) -> c e. ( EE ` N ) )
15 btwncom 
 |-  ( ( N e. NN /\ ( D e. ( EE ` N ) /\ A e. ( EE ` N ) /\ c e. ( EE ` N ) ) ) -> ( D Btwn <. A , c >. <-> D Btwn <. c , A >. ) )
16 7 13 9 14 15 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 ) ) ) ) -> ( D Btwn <. A , c >. <-> D Btwn <. c , A >. ) )
17 12 16 anbi12d 
 |-  ( ( ( 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 ) ) ) ) -> ( ( C Btwn <. A , d >. /\ D Btwn <. A , c >. ) <-> ( C Btwn <. d , A >. /\ D Btwn <. c , A >. ) ) )
18 6 17 imbitrid 
 |-  ( ( ( 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 ) ) ) ) -> ( ( ( ( ( A =/= B /\ B =/= 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 ) -> ( C Btwn <. d , A >. /\ D Btwn <. c , A >. ) ) )
19 axpasch 
 |-  ( ( N e. NN /\ ( d e. ( EE ` N ) /\ c e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( C Btwn <. d , A >. /\ D Btwn <. c , A >. ) -> E. e e. ( EE ` N ) ( e Btwn <. C , c >. /\ e Btwn <. D , d >. ) ) )
20 7 10 14 9 8 13 19 syl132anc 
 |-  ( ( ( 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 ) ) ) ) -> ( ( C Btwn <. d , A >. /\ D Btwn <. c , A >. ) -> E. e e. ( EE ` N ) ( e Btwn <. C , c >. /\ e Btwn <. D , d >. ) ) )
21 18 20 syld 
 |-  ( ( ( 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 ) ) ) ) -> ( ( ( ( ( A =/= B /\ B =/= 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 ) -> E. e e. ( EE ` N ) ( e Btwn <. C , c >. /\ e Btwn <. D , d >. ) ) )
22 21 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 ) ) ) ) /\ ( ( ( ( A =/= B /\ B =/= 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 ) ) -> E. e e. ( EE ` N ) ( e Btwn <. C , c >. /\ e Btwn <. D , d >. ) )
23 simpll1 
 |-  ( ( ( ( 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 ) ) -> N e. NN )
24 14 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 ) ) -> c e. ( EE ` N ) )
25 8 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 ) ) -> C e. ( EE ` N ) )
26 10 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 ) ) -> d e. ( EE ` N ) )
27 axsegcon 
 |-  ( ( N e. NN /\ ( c e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) -> E. p e. ( EE ` N ) ( C Btwn <. c , p >. /\ <. C , p >. Cgr <. C , d >. ) )
28 23 24 25 25 26 27 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 ) ) -> E. p e. ( EE ` N ) ( C Btwn <. c , p >. /\ <. C , p >. Cgr <. C , d >. ) )
29 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 ) ) -> e e. ( EE ` N ) )
30 axsegcon 
 |-  ( ( N e. NN /\ ( d e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ e e. ( EE ` N ) ) ) -> E. r e. ( EE ` N ) ( C Btwn <. d , r >. /\ <. C , r >. Cgr <. C , e >. ) )
31 23 26 25 25 29 30 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 ) ) -> E. r e. ( EE ` N ) ( C Btwn <. d , r >. /\ <. C , r >. Cgr <. C , e >. ) )
32 reeanv 
 |-  ( E. p e. ( EE ` N ) E. r e. ( EE ` N ) ( ( C Btwn <. c , p >. /\ <. C , p >. Cgr <. C , d >. ) /\ ( C Btwn <. d , r >. /\ <. C , r >. Cgr <. C , e >. ) ) <-> ( E. p e. ( EE ` N ) ( C Btwn <. c , p >. /\ <. C , p >. Cgr <. C , d >. ) /\ E. r e. ( EE ` N ) ( C Btwn <. d , r >. /\ <. C , r >. Cgr <. C , e >. ) ) )
33 28 31 32 sylanbrc 
 |-  ( ( ( ( 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 ) ) -> E. p e. ( EE ` N ) E. r e. ( EE ` N ) ( ( C Btwn <. c , p >. /\ <. C , p >. Cgr <. C , d >. ) /\ ( C Btwn <. d , r >. /\ <. C , r >. Cgr <. C , e >. ) ) )
34 33 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 ) ) /\ ( ( ( ( ( A =/= B /\ B =/= 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 ) /\ ( e Btwn <. C , c >. /\ e Btwn <. D , d >. ) ) ) -> E. p e. ( EE ` N ) E. r e. ( EE ` N ) ( ( C Btwn <. c , p >. /\ <. C , p >. Cgr <. C , d >. ) /\ ( C Btwn <. d , r >. /\ <. C , r >. Cgr <. C , e >. ) ) )
35 7 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 ) /\ r e. ( EE ` N ) ) ) -> N e. NN )
36 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 ) /\ r e. ( EE ` N ) ) ) -> p e. ( EE ` N ) )
37 simprr 
 |-  ( ( ( ( ( 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 ) /\ r e. ( EE ` N ) ) ) -> r e. ( EE ` N ) )
38 axsegcon 
 |-  ( ( N e. NN /\ ( p e. ( EE ` N ) /\ r e. ( EE ` N ) ) /\ ( r e. ( EE ` N ) /\ p e. ( EE ` N ) ) ) -> E. q e. ( EE ` N ) ( r Btwn <. p , q >. /\ <. r , q >. Cgr <. r , p >. ) )
39 35 36 37 37 36 38 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 ) /\ r e. ( EE ` N ) ) ) -> E. q e. ( EE ` N ) ( r Btwn <. p , q >. /\ <. r , q >. Cgr <. r , p >. ) )
40 39 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 ) /\ r e. ( EE ` N ) ) ) /\ ( ( ( ( ( ( A =/= B /\ B =/= 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 ) /\ ( 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 >. ) ) ) ) -> E. q e. ( EE ` N ) ( r Btwn <. p , q >. /\ <. r , q >. Cgr <. r , p >. ) )
41 simp-4l 
 |-  ( ( ( ( ( ( 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 ) /\ r e. ( EE ` N ) ) ) /\ q e. ( EE ` N ) ) -> ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) )
42 simplrl 
 |-  ( ( ( ( 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 ) ) -> ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) )
43 42 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 ) /\ r e. ( EE ` N ) ) ) /\ q e. ( EE ` N ) ) -> ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) )
44 10 ad3antrrr 
 |-  ( ( ( ( ( ( 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 ) /\ r e. ( EE ` N ) ) ) /\ q e. ( EE ` N ) ) -> d e. ( EE ` N ) )
45 simprrr 
 |-  ( ( ( 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 ) ) ) ) -> b e. ( EE ` N ) )
46 45 ad3antrrr 
 |-  ( ( ( ( ( ( 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 ) /\ r e. ( EE ` N ) ) ) /\ q e. ( EE ` N ) ) -> b e. ( EE ` N ) )
47 simpllr 
 |-  ( ( ( ( ( ( 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 ) /\ r e. ( EE ` N ) ) ) /\ q e. ( EE ` N ) ) -> e e. ( EE ` N ) )
48 44 46 47 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 ) /\ r e. ( EE ` N ) ) ) /\ q e. ( EE ` N ) ) -> ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ e e. ( EE ` N ) ) )
49 43 48 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 ) /\ r e. ( EE ` N ) ) ) /\ q 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 ) ) ) )
50 simplrl 
 |-  ( ( ( ( ( ( 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 ) /\ r e. ( EE ` N ) ) ) /\ q e. ( EE ` N ) ) -> p e. ( EE ` N ) )
51 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 ) /\ r e. ( EE ` N ) ) ) /\ q e. ( EE ` N ) ) -> q e. ( EE ` N ) )
52 simplrr 
 |-  ( ( ( ( ( ( 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 ) /\ r e. ( EE ` N ) ) ) /\ q e. ( EE ` N ) ) -> r e. ( EE ` N ) )
53 50 51 52 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 ) /\ r e. ( EE ` N ) ) ) /\ q e. ( EE ` N ) ) -> ( p e. ( EE ` N ) /\ q e. ( EE ` N ) /\ r e. ( EE ` N ) ) )
54 41 49 53 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 ) /\ r e. ( EE ` N ) ) ) /\ q 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 ) ) ) /\ ( p e. ( EE ` N ) /\ q e. ( EE ` N ) /\ r e. ( EE ` N ) ) ) )
55 simp1ll 
 |-  ( ( ( ( A =/= B /\ B =/= 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 >. ) ) ) -> A =/= B )
56 55 ad3antrrr 
 |-  ( ( ( ( ( ( ( A =/= B /\ B =/= 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 ) /\ ( 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 >. ) ) ) -> A =/= B )
57 56 adantr 
 |-  ( ( ( ( ( ( ( ( A =/= B /\ B =/= 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 ) /\ ( 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 )
58 simp1lr 
 |-  ( ( ( ( A =/= B /\ B =/= 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 =/= C )
59 58 ad3antrrr 
 |-  ( ( ( ( ( ( ( A =/= B /\ B =/= 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 ) /\ ( 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 >. ) ) ) -> B =/= C )
60 59 adantr 
 |-  ( ( ( ( ( ( ( ( A =/= B /\ B =/= 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 ) /\ ( 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 =/= C )
61 simpllr 
 |-  ( ( ( ( ( ( ( A =/= B /\ B =/= 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 ) /\ ( 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 >. ) ) ) -> C =/= c )
62 61 adantr 
 |-  ( ( ( ( ( ( ( ( A =/= B /\ B =/= 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 ) /\ ( 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 )
63 57 60 62 3jca 
 |-  ( ( ( ( ( ( ( ( A =/= B /\ B =/= 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 ) /\ ( 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 ) )
64 simpl1r 
 |-  ( ( ( ( ( A =/= B /\ B =/= 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 ) -> ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) )
65 64 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( A =/= B /\ B =/= 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 ) /\ ( 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 >. /\ B Btwn <. A , D >. ) )
66 63 65 jca 
 |-  ( ( ( ( ( ( ( ( A =/= B /\ B =/= 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 ) /\ ( 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 >. ) ) )
67 simpll2 
 |-  ( ( ( ( ( ( A =/= B /\ B =/= 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 ) /\ ( e Btwn <. C , c >. /\ e Btwn <. D , d >. ) ) -> ( ( D Btwn <. A , c >. /\ <. D , c >. Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >. Cgr <. C , D >. ) ) )
68 67 ad2antrr 
 |-  ( ( ( ( ( ( ( ( A =/= B /\ B =/= 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 ) /\ ( 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 >. /\ <. D , c >. Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >. Cgr <. C , D >. ) ) )
69 simpl3l 
 |-  ( ( ( ( ( A =/= B /\ B =/= 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 ) -> ( c Btwn <. A , b >. /\ <. c , b >. Cgr <. C , B >. ) )
70 69 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( A =/= B /\ B =/= 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 ) /\ ( 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 >. /\ <. c , b >. Cgr <. C , B >. ) )
71 simpl3r 
 |-  ( ( ( ( ( A =/= B /\ B =/= 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 ) -> ( d Btwn <. A , b >. /\ <. d , b >. Cgr <. D , B >. ) )
72 71 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( A =/= B /\ B =/= 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 ) /\ ( 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 >. /\ <. d , b >. Cgr <. D , B >. ) )
73 70 72 jca 
 |-  ( ( ( ( ( ( ( ( A =/= B /\ B =/= 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 ) /\ ( 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 >. /\ <. c , b >. Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >. Cgr <. D , B >. ) ) )
74 66 68 73 3jca 
 |-  ( ( ( ( ( ( ( ( A =/= B /\ B =/= 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 ) /\ ( 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 >. ) ) ) )
75 simpllr 
 |-  ( ( ( ( ( ( ( ( A =/= B /\ B =/= 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 ) /\ ( 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 >. ) )
76 simplrl 
 |-  ( ( ( ( ( ( ( ( A =/= B /\ B =/= 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 ) /\ ( 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 , p >. Cgr <. C , d >. ) )
77 simplrr 
 |-  ( ( ( ( ( ( ( ( A =/= B /\ B =/= 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 ) /\ ( 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 >. /\ <. C , r >. Cgr <. C , e >. ) )
78 simpr 
 |-  ( ( ( ( ( ( ( ( A =/= B /\ B =/= 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 ) /\ ( 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 Btwn <. p , q >. /\ <. r , q >. Cgr <. r , p >. ) )
79 76 77 78 3jca 
 |-  ( ( ( ( ( ( ( ( A =/= B /\ B =/= 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 ) /\ ( 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 , p >. Cgr <. C , d >. ) /\ ( C Btwn <. d , r >. /\ <. C , r >. Cgr <. C , e >. ) /\ ( r Btwn <. p , q >. /\ <. r , q >. Cgr <. r , p >. ) ) )
80 74 75 79 jca32 
 |-  ( ( ( ( ( ( ( ( A =/= B /\ B =/= 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 ) /\ ( 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 >. ) /\ ( ( 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 >. ) ) ) ) )
81 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 )
82 54 80 81 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 ) /\ r e. ( EE ` N ) ) ) /\ q e. ( EE ` N ) ) /\ ( ( ( ( ( ( ( A =/= B /\ B =/= 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 ) /\ ( 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 )
83 82 an4s 
 |-  ( ( ( ( ( ( ( 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 ) /\ r e. ( EE ` N ) ) ) /\ ( ( ( ( ( ( A =/= B /\ B =/= 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 ) /\ ( 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 >. ) ) ) ) /\ ( q e. ( EE ` N ) /\ ( r Btwn <. p , q >. /\ <. r , q >. Cgr <. r , p >. ) ) ) -> D = d )
84 40 83 rexlimddv 
 |-  ( ( ( ( ( ( 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 ) /\ r e. ( EE ` N ) ) ) /\ ( ( ( ( ( ( A =/= B /\ B =/= 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 ) /\ ( 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 >. ) ) ) ) -> D = d )
85 84 an4s 
 |-  ( ( ( ( ( ( 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 ) /\ ( 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 ) /\ ( e Btwn <. C , c >. /\ e Btwn <. D , d >. ) ) ) /\ ( ( p e. ( EE ` N ) /\ r e. ( EE ` N ) ) /\ ( ( C Btwn <. c , p >. /\ <. C , p >. Cgr <. C , d >. ) /\ ( C Btwn <. d , r >. /\ <. C , r >. Cgr <. C , e >. ) ) ) ) -> D = d )
86 85 exp32 
 |-  ( ( ( ( ( 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 ) /\ ( 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 ) /\ ( e Btwn <. C , c >. /\ e Btwn <. D , d >. ) ) ) -> ( ( p e. ( EE ` N ) /\ r e. ( EE ` N ) ) -> ( ( ( C Btwn <. c , p >. /\ <. C , p >. Cgr <. C , d >. ) /\ ( C Btwn <. d , r >. /\ <. C , r >. Cgr <. C , e >. ) ) -> D = d ) ) )
87 86 rexlimdvv 
 |-  ( ( ( ( ( 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 ) /\ ( 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 ) /\ ( e Btwn <. C , c >. /\ e Btwn <. D , d >. ) ) ) -> ( E. p e. ( EE ` N ) E. r e. ( EE ` N ) ( ( C Btwn <. c , p >. /\ <. C , p >. Cgr <. C , d >. ) /\ ( C Btwn <. d , r >. /\ <. C , r >. Cgr <. C , e >. ) ) -> D = d ) )
88 34 87 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 ) ) /\ ( ( ( ( ( A =/= B /\ B =/= 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 ) /\ ( e Btwn <. C , c >. /\ e Btwn <. D , d >. ) ) ) -> D = d )
89 88 an4s 
 |-  ( ( ( ( ( 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 ) ) ) ) /\ ( ( ( ( A =/= B /\ B =/= 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 ) ) /\ ( e e. ( EE ` N ) /\ ( e Btwn <. C , c >. /\ e Btwn <. D , d >. ) ) ) -> D = d )
90 22 89 rexlimddv 
 |-  ( ( ( ( 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 ) ) ) ) /\ ( ( ( ( A =/= B /\ B =/= 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 ) ) -> D = d )
91 90 expr 
 |-  ( ( ( ( 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 ) ) ) ) /\ ( ( ( A =/= B /\ B =/= 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 -> D = d ) )
92 1 91 biimtrrid 
 |-  ( ( ( ( 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 ) ) ) ) /\ ( ( ( A =/= B /\ B =/= 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 -> D = d ) )
93 92 orrd 
 |-  ( ( ( ( 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 ) ) ) ) /\ ( ( ( A =/= B /\ B =/= 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 \/ D = d ) )