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
|
syl5bi |
|- ( ( ( ( N e. NN /\ ( 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 >. ) ) |