Metamath Proof Explorer

Theorem btwnconn1lem14

Description: Lemma for btwnconn1 . Final statement of the theorem when B =/= C . (Contributed by Scott Fenton, 9-Oct-2013)

Ref Expression
Assertion btwnconn1lem14 
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( ( A =/= B /\ B =/= C ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) ) -> ( C Btwn <. A , D >. \/ D Btwn <. A , C >. ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> N e. NN )
2 simp2l 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
3 simp3r 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> D e. ( EE ` N ) )
4 simp3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) )
5 axsegcon 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> E. c e. ( EE ` N ) ( D Btwn <. A , c >. /\ <. D , c >. Cgr <. C , D >. ) )
6 1 2 3 4 5 syl121anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> E. c e. ( EE ` N ) ( D Btwn <. A , c >. /\ <. D , c >. Cgr <. C , D >. ) )
7 simp3l 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
8 axsegcon 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> E. d e. ( EE ` N ) ( C Btwn <. A , d >. /\ <. C , d >. Cgr <. C , D >. ) )
9 1 2 7 4 8 syl121anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> E. d e. ( EE ` N ) ( C Btwn <. A , d >. /\ <. C , d >. Cgr <. C , D >. ) )
10 reeanv 
 |-  ( E. c e. ( EE ` N ) E. d e. ( EE ` N ) ( ( D Btwn <. A , c >. /\ <. D , c >. Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >. Cgr <. C , D >. ) ) <-> ( E. c e. ( EE ` N ) ( D Btwn <. A , c >. /\ <. D , c >. Cgr <. C , D >. ) /\ E. d e. ( EE ` N ) ( C Btwn <. A , d >. /\ <. C , d >. Cgr <. C , D >. ) ) )
11 6 9 10 sylanbrc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> E. c e. ( EE ` N ) E. d e. ( EE ` N ) ( ( D Btwn <. A , c >. /\ <. D , c >. Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >. Cgr <. C , D >. ) ) )
12 11 adantr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( ( A =/= B /\ B =/= C ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) ) -> E. c e. ( EE ` N ) E. d e. ( EE ` N ) ( ( D Btwn <. A , c >. /\ <. D , c >. Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >. Cgr <. C , D >. ) ) )
13 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 ) ) ) -> N e. NN )
14 simpl2l 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( c e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
15 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 ) ) ) -> c e. ( EE ` N ) )
16 simpl3l 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( c e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
17 simpl2r 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( c e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
18 axsegcon 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> E. b e. ( EE ` N ) ( c Btwn <. A , b >. /\ <. c , b >. Cgr <. C , B >. ) )
19 13 14 15 16 17 18 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 ) ) ) -> E. b e. ( EE ` N ) ( c Btwn <. A , b >. /\ <. c , b >. Cgr <. C , B >. ) )
20 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 ) ) ) -> d e. ( EE ` N ) )
21 simpl3r 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( c e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) -> D e. ( EE ` N ) )
22 axsegcon 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ d e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> E. x e. ( EE ` N ) ( d Btwn <. A , x >. /\ <. d , x >. Cgr <. D , B >. ) )
23 13 14 20 21 17 22 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 ) ) ) -> E. x e. ( EE ` N ) ( d Btwn <. A , x >. /\ <. d , x >. Cgr <. D , B >. ) )
24 19 23 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 ) ) ) -> ( E. b e. ( EE ` N ) ( c Btwn <. A , b >. /\ <. c , b >. Cgr <. C , B >. ) /\ E. x e. ( EE ` N ) ( d Btwn <. A , x >. /\ <. d , x >. Cgr <. D , B >. ) ) )
25 24 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 ) ) ) /\ ( ( ( 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 >. ) ) ) ) -> ( E. b e. ( EE ` N ) ( c Btwn <. A , b >. /\ <. c , b >. Cgr <. C , B >. ) /\ E. x e. ( EE ` N ) ( d Btwn <. A , x >. /\ <. d , x >. Cgr <. D , B >. ) ) )
26 reeanv 
 |-  ( E. b e. ( EE ` N ) E. x e. ( EE ` N ) ( ( c Btwn <. A , b >. /\ <. c , b >. Cgr <. C , B >. ) /\ ( d Btwn <. A , x >. /\ <. d , x >. Cgr <. D , B >. ) ) <-> ( E. b e. ( EE ` N ) ( c Btwn <. A , b >. /\ <. c , b >. Cgr <. C , B >. ) /\ E. x e. ( EE ` N ) ( d Btwn <. A , x >. /\ <. d , x >. Cgr <. D , B >. ) ) )
27 25 26 sylibr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( c e. ( EE ` N ) /\ d 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 >. ) ) ) ) -> E. b e. ( EE ` N ) E. x e. ( EE ` N ) ( ( c Btwn <. A , b >. /\ <. c , b >. Cgr <. C , B >. ) /\ ( d Btwn <. A , x >. /\ <. d , x >. Cgr <. D , B >. ) ) )
28 13 14 17 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 ) ) ) -> ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) )
29 28 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 ) /\ x e. ( EE ` N ) ) ) -> ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) )
30 16 21 15 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 ) ) ) -> ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) )
31 30 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 ) /\ x e. ( EE ` N ) ) ) -> ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) )
32 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 ) /\ x e. ( EE ` N ) ) ) -> d e. ( EE ` N ) )
33 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 ) /\ x e. ( EE ` N ) ) ) -> b e. ( EE ` N ) )
34 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 ) /\ x e. ( EE ` N ) ) ) -> x e. ( EE ` N ) )
35 32 33 34 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 ) /\ x e. ( EE ` N ) ) ) -> ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ x e. ( EE ` N ) ) )
36 29 31 35 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 ) /\ x 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 ) /\ x e. ( EE ` N ) ) ) )
37 simpll 
 |-  ( ( ( ( ( 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 , x >. /\ <. d , x >. Cgr <. D , B >. ) ) ) -> ( ( A =/= B /\ B =/= C ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) )
38 simplr 
 |-  ( ( ( ( ( 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 , x >. /\ <. d , x >. Cgr <. D , B >. ) ) ) -> ( ( D Btwn <. A , c >. /\ <. D , c >. Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >. Cgr <. C , D >. ) ) )
39 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 , x >. /\ <. d , x >. Cgr <. D , B >. ) ) ) -> ( ( c Btwn <. A , b >. /\ <. c , b >. Cgr <. C , B >. ) /\ ( d Btwn <. A , x >. /\ <. d , x >. Cgr <. D , B >. ) ) )
40 37 38 39 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 , x >. /\ <. d , x >. Cgr <. D , B >. ) ) ) -> ( ( ( 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 , x >. /\ <. d , x >. Cgr <. D , B >. ) ) ) )
41 btwnconn1lem2 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ c e. ( EE ` N ) ) /\ ( d e. ( EE ` N ) /\ b e. ( EE ` N ) /\ x 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 , x >. /\ <. d , x >. Cgr <. D , B >. ) ) ) ) -> x = b )
42 36 40 41 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 ) /\ x 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 , x >. /\ <. d , x >. Cgr <. D , B >. ) ) ) ) -> x = b )
43 opeq2 
 |-  ( x = b -> <. A , x >. = <. A , b >. )
44 43 breq2d 
 |-  ( x = b -> ( d Btwn <. A , x >. <-> d Btwn <. A , b >. ) )
45 opeq2 
 |-  ( x = b -> <. d , x >. = <. d , b >. )
46 45 breq1d 
 |-  ( x = b -> ( <. d , x >. Cgr <. D , B >. <-> <. d , b >. Cgr <. D , B >. ) )
47 44 46 anbi12d 
 |-  ( x = b -> ( ( d Btwn <. A , x >. /\ <. d , x >. Cgr <. D , B >. ) <-> ( d Btwn <. A , b >. /\ <. d , b >. Cgr <. D , B >. ) ) )
48 47 anbi2d 
 |-  ( x = b -> ( ( ( c Btwn <. A , b >. /\ <. c , b >. Cgr <. C , B >. ) /\ ( d Btwn <. A , x >. /\ <. d , x >. Cgr <. D , B >. ) ) <-> ( ( c Btwn <. A , b >. /\ <. c , b >. Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >. Cgr <. D , B >. ) ) ) )
49 48 anbi2d 
 |-  ( x = b -> ( ( ( ( ( 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 , x >. /\ <. d , x >. Cgr <. D , B >. ) ) ) <-> ( ( ( ( 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 >. ) ) ) ) )
50 49 biimpac 
 |-  ( ( ( ( ( ( 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 , x >. /\ <. d , x >. Cgr <. D , B >. ) ) ) /\ x = b ) -> ( ( ( ( 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 >. ) ) ) )
51 32 33 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 ) /\ x e. ( EE ` N ) ) ) -> ( d e. ( EE ` N ) /\ b e. ( EE ` N ) ) )
52 29 31 51 jca32 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( c e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) /\ ( b e. ( EE ` N ) /\ x 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 ) ) ) ) )
53 simpll 
 |-  ( ( ( ( ( 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 /\ B =/= C ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) )
54 simplr 
 |-  ( ( ( ( ( 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 >. /\ <. D , c >. Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >. Cgr <. C , D >. ) ) )
55 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 Btwn <. A , b >. /\ <. c , b >. Cgr <. C , B >. ) /\ ( d Btwn <. A , b >. /\ <. d , b >. Cgr <. D , B >. ) ) )
56 53 54 55 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 >. ) ) ) -> ( ( ( 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 >. ) ) ) )
57 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 ) )
58 52 56 57 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 ) /\ x 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 ) )
59 58 ex 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( c e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) /\ ( b e. ( EE ` N ) /\ x 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 ) ) )
60 50 59 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 ) /\ x 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 , x >. /\ <. d , x >. Cgr <. D , B >. ) ) ) /\ x = b ) -> ( C = c \/ D = d ) ) )
61 60 expdimp 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( c e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) /\ ( b e. ( EE ` N ) /\ x 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 , x >. /\ <. d , x >. Cgr <. D , B >. ) ) ) ) -> ( x = b -> ( C = c \/ D = d ) ) )
62 42 61 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 ) /\ x 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 , x >. /\ <. d , x >. Cgr <. D , B >. ) ) ) ) -> ( C = c \/ D = d ) )
63 62 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 ) ) ) /\ ( ( ( 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 >. ) ) ) ) /\ ( ( b e. ( EE ` N ) /\ x e. ( EE ` N ) ) /\ ( ( c Btwn <. A , b >. /\ <. c , b >. Cgr <. C , B >. ) /\ ( d Btwn <. A , x >. /\ <. d , x >. Cgr <. D , B >. ) ) ) ) -> ( C = c \/ D = d ) )
64 63 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 ) ) ) /\ ( ( ( 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 >. ) ) ) ) -> ( ( b e. ( EE ` N ) /\ x e. ( EE ` N ) ) -> ( ( ( c Btwn <. A , b >. /\ <. c , b >. Cgr <. C , B >. ) /\ ( d Btwn <. A , x >. /\ <. d , x >. Cgr <. D , B >. ) ) -> ( C = c \/ D = d ) ) ) )
65 64 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 ) ) ) /\ ( ( ( 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 >. ) ) ) ) -> ( E. b e. ( EE ` N ) E. x e. ( EE ` N ) ( ( c Btwn <. A , b >. /\ <. c , b >. Cgr <. C , B >. ) /\ ( d Btwn <. A , x >. /\ <. d , x >. Cgr <. D , B >. ) ) -> ( C = c \/ D = d ) ) )
66 27 65 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 ) ) ) /\ ( ( ( 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 = c \/ D = d ) )
67 orcom 
 |-  ( ( C = c \/ D = d ) <-> ( D = d \/ C = c ) )
68 simprrl 
 |-  ( ( ( ( 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 , d >. )
69 68 adantl 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( c e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) /\ ( ( ( 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 , d >. )
70 opeq2 
 |-  ( D = d -> <. A , D >. = <. A , d >. )
71 70 breq2d 
 |-  ( D = d -> ( C Btwn <. A , D >. <-> C Btwn <. A , d >. ) )
72 69 71 syl5ibrcom 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( c e. ( EE ` N ) /\ d 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 >. ) ) ) ) -> ( D = d -> C Btwn <. A , D >. ) )
73 simprll 
 |-  ( ( ( ( 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 >. ) ) ) -> D Btwn <. A , c >. )
74 73 adantl 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( c e. ( EE ` N ) /\ d e. ( EE ` N ) ) ) /\ ( ( ( 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 >. ) ) ) ) -> D Btwn <. A , c >. )
75 opeq2 
 |-  ( C = c -> <. A , C >. = <. A , c >. )
76 75 breq2d 
 |-  ( C = c -> ( D Btwn <. A , C >. <-> D Btwn <. A , c >. ) )
77 74 76 syl5ibrcom 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( c e. ( EE ` N ) /\ d 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 = c -> D Btwn <. A , C >. ) )
78 72 77 orim12d 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( c e. ( EE ` N ) /\ d 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 >. ) ) ) ) -> ( ( D = d \/ C = c ) -> ( C Btwn <. A , D >. \/ D Btwn <. A , C >. ) ) )
79 67 78 biimtrid 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( c e. ( EE ` N ) /\ d 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 = c \/ D = d ) -> ( C Btwn <. A , D >. \/ D Btwn <. A , C >. ) ) )
80 66 79 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 ) ) ) /\ ( ( ( 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 , D >. \/ D Btwn <. A , C >. ) )
81 80 an4s 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( ( A =/= B /\ B =/= C ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) ) /\ ( ( c e. ( EE ` N ) /\ d e. ( EE ` N ) ) /\ ( ( D Btwn <. A , c >. /\ <. D , c >. Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >. Cgr <. C , D >. ) ) ) ) -> ( C Btwn <. A , D >. \/ D Btwn <. A , C >. ) )
82 81 exp32 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( ( A =/= B /\ B =/= C ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) ) -> ( ( c e. ( EE ` N ) /\ d e. ( EE ` N ) ) -> ( ( ( D Btwn <. A , c >. /\ <. D , c >. Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >. Cgr <. C , D >. ) ) -> ( C Btwn <. A , D >. \/ D Btwn <. A , C >. ) ) ) )
83 82 rexlimdvv 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( ( A =/= B /\ B =/= C ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) ) -> ( E. c e. ( EE ` N ) E. d e. ( EE ` N ) ( ( D Btwn <. A , c >. /\ <. D , c >. Cgr <. C , D >. ) /\ ( C Btwn <. A , d >. /\ <. C , d >. Cgr <. C , D >. ) ) -> ( C Btwn <. A , D >. \/ D Btwn <. A , C >. ) ) )
84 12 83 mpd 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( ( A =/= B /\ B =/= C ) /\ ( B Btwn <. A , C >. /\ B Btwn <. A , D >. ) ) ) -> ( C Btwn <. A , D >. \/ D Btwn <. A , C >. ) )