Metamath Proof Explorer

Theorem brsegle2

Description: Alternate characterization of segment comparison. Theorem 5.5 of Schwabhauser p. 41-42. (Contributed by Scott Fenton, 11-Oct-2013)

Ref Expression
Assertion brsegle2 
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. A , B >. Seg<_ <. C , D >. <-> E. x e. ( EE ` N ) ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) ) )

Proof

Step Hyp Ref Expression
1 brsegle 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. A , B >. Seg<_ <. C , D >. <-> E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) )
2 simprl 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) -> y Btwn <. C , D >. )
3 simpl1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) -> N e. NN )
4 simpl3l 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) -> C e. ( EE ` N ) )
5 simpl3r 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) -> D e. ( EE ` N ) )
6 simpr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) -> y e. ( EE ` N ) )
7 btwncolinear2 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) -> ( y Btwn <. C , D >. -> C Colinear <. y , D >. ) )
8 3 4 5 6 7 syl13anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) -> ( y Btwn <. C , D >. -> C Colinear <. y , D >. ) )
9 8 adantr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) -> ( y Btwn <. C , D >. -> C Colinear <. y , D >. ) )
10 2 9 mpd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) -> C Colinear <. y , D >. )
11 simpl2l 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) -> A e. ( EE ` N ) )
12 simpl2r 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) -> B e. ( EE ` N ) )
13 simprr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) -> <. A , B >. Cgr <. C , y >. )
14 3 11 12 4 6 13 cgrcomand 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) -> <. C , y >. Cgr <. A , B >. )
15 simpl2 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) -> ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) )
16 lineext 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ y e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( ( C Colinear <. y , D >. /\ <. C , y >. Cgr <. A , B >. ) -> E. x e. ( EE ` N ) <. C , <. y , D >. >. Cgr3 <. A , <. B , x >. >. ) )
17 3 4 6 5 15 16 syl131anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) -> ( ( C Colinear <. y , D >. /\ <. C , y >. Cgr <. A , B >. ) -> E. x e. ( EE ` N ) <. C , <. y , D >. >. Cgr3 <. A , <. B , x >. >. ) )
18 17 adantr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) -> ( ( C Colinear <. y , D >. /\ <. C , y >. Cgr <. A , B >. ) -> E. x e. ( EE ` N ) <. C , <. y , D >. >. Cgr3 <. A , <. B , x >. >. ) )
19 10 14 18 mp2and 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) -> E. x e. ( EE ` N ) <. C , <. y , D >. >. Cgr3 <. A , <. B , x >. >. )
20 an32 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ y 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 ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) )
21 simpll1 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) -> N e. NN )
22 simpl3l 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> C e. ( EE ` N ) )
23 22 adantr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) -> C e. ( EE ` N ) )
24 simpr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) -> y e. ( EE ` N ) )
25 simpl3r 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> D e. ( EE ` N ) )
26 25 adantr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) -> D e. ( EE ` N ) )
27 simpl2l 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> A e. ( EE ` N ) )
28 27 adantr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) -> A e. ( EE ` N ) )
29 simpl2r 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> B e. ( EE ` N ) )
30 29 adantr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) -> B e. ( EE ` N ) )
31 simplr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) -> x e. ( EE ` N ) )
32 brcgr3 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ y e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) -> ( <. C , <. y , D >. >. Cgr3 <. A , <. B , x >. >. <-> ( <. C , y >. Cgr <. A , B >. /\ <. C , D >. Cgr <. A , x >. /\ <. y , D >. Cgr <. B , x >. ) ) )
33 21 23 24 26 28 30 31 32 syl133anc 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) -> ( <. C , <. y , D >. >. Cgr3 <. A , <. B , x >. >. <-> ( <. C , y >. Cgr <. A , B >. /\ <. C , D >. Cgr <. A , x >. /\ <. y , D >. Cgr <. B , x >. ) ) )
34 33 adantr 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) -> ( <. C , <. y , D >. >. Cgr3 <. A , <. B , x >. >. <-> ( <. C , y >. Cgr <. A , B >. /\ <. C , D >. Cgr <. A , x >. /\ <. y , D >. Cgr <. B , x >. ) ) )
35 simp2l 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( <. C , y >. Cgr <. A , B >. /\ <. C , D >. Cgr <. A , x >. /\ <. y , D >. Cgr <. B , x >. ) ) -> y Btwn <. C , D >. )
36 simp3 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( <. C , y >. Cgr <. A , B >. /\ <. C , D >. Cgr <. A , x >. /\ <. y , D >. Cgr <. B , x >. ) ) -> ( <. C , y >. Cgr <. A , B >. /\ <. C , D >. Cgr <. A , x >. /\ <. y , D >. Cgr <. B , x >. ) )
37 33 3ad2ant1 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( <. C , y >. Cgr <. A , B >. /\ <. C , D >. Cgr <. A , x >. /\ <. y , D >. Cgr <. B , x >. ) ) -> ( <. C , <. y , D >. >. Cgr3 <. A , <. B , x >. >. <-> ( <. C , y >. Cgr <. A , B >. /\ <. C , D >. Cgr <. A , x >. /\ <. y , D >. Cgr <. B , x >. ) ) )
38 36 37 mpbird 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( <. C , y >. Cgr <. A , B >. /\ <. C , D >. Cgr <. A , x >. /\ <. y , D >. Cgr <. B , x >. ) ) -> <. C , <. y , D >. >. Cgr3 <. A , <. B , x >. >. )
39 btwnxfr 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ y e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) -> ( ( y Btwn <. C , D >. /\ <. C , <. y , D >. >. Cgr3 <. A , <. B , x >. >. ) -> B Btwn <. A , x >. ) )
40 21 23 24 26 28 30 31 39 syl133anc 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) -> ( ( y Btwn <. C , D >. /\ <. C , <. y , D >. >. Cgr3 <. A , <. B , x >. >. ) -> B Btwn <. A , x >. ) )
41 40 3ad2ant1 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( <. C , y >. Cgr <. A , B >. /\ <. C , D >. Cgr <. A , x >. /\ <. y , D >. Cgr <. B , x >. ) ) -> ( ( y Btwn <. C , D >. /\ <. C , <. y , D >. >. Cgr3 <. A , <. B , x >. >. ) -> B Btwn <. A , x >. ) )
42 35 38 41 mp2and 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( <. C , y >. Cgr <. A , B >. /\ <. C , D >. Cgr <. A , x >. /\ <. y , D >. Cgr <. B , x >. ) ) -> B Btwn <. A , x >. )
43 simp32 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( <. C , y >. Cgr <. A , B >. /\ <. C , D >. Cgr <. A , x >. /\ <. y , D >. Cgr <. B , x >. ) ) -> <. C , D >. Cgr <. A , x >. )
44 cgrcom 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( A e. ( EE ` N ) /\ x e. ( EE ` N ) ) ) -> ( <. C , D >. Cgr <. A , x >. <-> <. A , x >. Cgr <. C , D >. ) )
45 21 23 26 28 31 44 syl122anc 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) -> ( <. C , D >. Cgr <. A , x >. <-> <. A , x >. Cgr <. C , D >. ) )
46 45 3ad2ant1 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( <. C , y >. Cgr <. A , B >. /\ <. C , D >. Cgr <. A , x >. /\ <. y , D >. Cgr <. B , x >. ) ) -> ( <. C , D >. Cgr <. A , x >. <-> <. A , x >. Cgr <. C , D >. ) )
47 43 46 mpbid 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( <. C , y >. Cgr <. A , B >. /\ <. C , D >. Cgr <. A , x >. /\ <. y , D >. Cgr <. B , x >. ) ) -> <. A , x >. Cgr <. C , D >. )
48 42 47 jca 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( <. C , y >. Cgr <. A , B >. /\ <. C , D >. Cgr <. A , x >. /\ <. y , D >. Cgr <. B , x >. ) ) -> ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) )
49 48 3expia 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) -> ( ( <. C , y >. Cgr <. A , B >. /\ <. C , D >. Cgr <. A , x >. /\ <. y , D >. Cgr <. B , x >. ) -> ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) ) )
50 34 49 sylbid 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) -> ( <. C , <. y , D >. >. Cgr3 <. A , <. B , x >. >. -> ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) ) )
51 20 50 sylanb 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ x e. ( EE ` N ) ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) -> ( <. C , <. y , D >. >. Cgr3 <. A , <. B , x >. >. -> ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) ) )
52 51 an32s 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) /\ x e. ( EE ` N ) ) -> ( <. C , <. y , D >. >. Cgr3 <. A , <. B , x >. >. -> ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) ) )
53 52 reximdva 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) -> ( E. x e. ( EE ` N ) <. C , <. y , D >. >. Cgr3 <. A , <. B , x >. >. -> E. x e. ( EE ` N ) ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) ) )
54 19 53 mpd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ y e. ( EE ` N ) ) /\ ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) -> E. x e. ( EE ` N ) ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) )
55 54 rexlimdva2 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) -> E. x e. ( EE ` N ) ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) ) )
56 simprl 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) ) -> B Btwn <. A , x >. )
57 simpll1 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) ) -> N e. NN )
58 27 adantr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) ) -> A e. ( EE ` N ) )
59 simplr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) ) -> x e. ( EE ` N ) )
60 29 adantr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) ) -> B e. ( EE ` N ) )
61 btwncolinear1 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ x e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( B Btwn <. A , x >. -> A Colinear <. x , B >. ) )
62 57 58 59 60 61 syl13anc 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) ) -> ( B Btwn <. A , x >. -> A Colinear <. x , B >. ) )
63 56 62 mpd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) ) -> A Colinear <. x , B >. )
64 simprr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) ) -> <. A , x >. Cgr <. C , D >. )
65 simpl1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> N e. NN )
66 simpr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> x e. ( EE ` N ) )
67 simpl3 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) )
68 lineext 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ x e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( A Colinear <. x , B >. /\ <. A , x >. Cgr <. C , D >. ) -> E. y e. ( EE ` N ) <. A , <. x , B >. >. Cgr3 <. C , <. D , y >. >. ) )
69 65 27 66 29 67 68 syl131anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( ( A Colinear <. x , B >. /\ <. A , x >. Cgr <. C , D >. ) -> E. y e. ( EE ` N ) <. A , <. x , B >. >. Cgr3 <. C , <. D , y >. >. ) )
70 69 adantr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) ) -> ( ( A Colinear <. x , B >. /\ <. A , x >. Cgr <. C , D >. ) -> E. y e. ( EE ` N ) <. A , <. x , B >. >. Cgr3 <. C , <. D , y >. >. ) )
71 63 64 70 mp2and 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) ) -> E. y e. ( EE ` N ) <. A , <. x , B >. >. Cgr3 <. C , <. D , y >. >. )
72 27 66 29 3jca 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( A e. ( EE ` N ) /\ x e. ( EE ` N ) /\ B e. ( EE ` N ) ) )
73 72 adantr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) -> ( A e. ( EE ` N ) /\ x e. ( EE ` N ) /\ B e. ( EE ` N ) ) )
74 brcgr3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ x e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) -> ( <. A , <. x , B >. >. Cgr3 <. C , <. D , y >. >. <-> ( <. A , x >. Cgr <. C , D >. /\ <. A , B >. Cgr <. C , y >. /\ <. x , B >. Cgr <. D , y >. ) ) )
75 21 73 23 26 24 74 syl113anc 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) -> ( <. A , <. x , B >. >. Cgr3 <. C , <. D , y >. >. <-> ( <. A , x >. Cgr <. C , D >. /\ <. A , B >. Cgr <. C , y >. /\ <. x , B >. Cgr <. D , y >. ) ) )
76 75 adantr 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) /\ ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) ) -> ( <. A , <. x , B >. >. Cgr3 <. C , <. D , y >. >. <-> ( <. A , x >. Cgr <. C , D >. /\ <. A , B >. Cgr <. C , y >. /\ <. x , B >. Cgr <. D , y >. ) ) )
77 simp2l 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) /\ ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) /\ ( <. A , x >. Cgr <. C , D >. /\ <. A , B >. Cgr <. C , y >. /\ <. x , B >. Cgr <. D , y >. ) ) -> B Btwn <. A , x >. )
78 simp32 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) /\ ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) /\ ( <. A , x >. Cgr <. C , D >. /\ <. A , B >. Cgr <. C , y >. /\ <. x , B >. Cgr <. D , y >. ) ) -> <. A , B >. Cgr <. C , y >. )
79 simp2r 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) /\ ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) /\ ( <. A , x >. Cgr <. C , D >. /\ <. A , B >. Cgr <. C , y >. /\ <. x , B >. Cgr <. D , y >. ) ) -> <. A , x >. Cgr <. C , D >. )
80 simp33 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) /\ ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) /\ ( <. A , x >. Cgr <. C , D >. /\ <. A , B >. Cgr <. C , y >. /\ <. x , B >. Cgr <. D , y >. ) ) -> <. x , B >. Cgr <. D , y >. )
81 cgrcomlr 
 |-  ( ( N e. NN /\ ( x e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) -> ( <. x , B >. Cgr <. D , y >. <-> <. B , x >. Cgr <. y , D >. ) )
82 21 31 30 26 24 81 syl122anc 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) -> ( <. x , B >. Cgr <. D , y >. <-> <. B , x >. Cgr <. y , D >. ) )
83 82 3ad2ant1 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) /\ ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) /\ ( <. A , x >. Cgr <. C , D >. /\ <. A , B >. Cgr <. C , y >. /\ <. x , B >. Cgr <. D , y >. ) ) -> ( <. x , B >. Cgr <. D , y >. <-> <. B , x >. Cgr <. y , D >. ) )
84 80 83 mpbid 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) /\ ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) /\ ( <. A , x >. Cgr <. C , D >. /\ <. A , B >. Cgr <. C , y >. /\ <. x , B >. Cgr <. D , y >. ) ) -> <. B , x >. Cgr <. y , D >. )
85 78 79 84 3jca 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) /\ ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) /\ ( <. A , x >. Cgr <. C , D >. /\ <. A , B >. Cgr <. C , y >. /\ <. x , B >. Cgr <. D , y >. ) ) -> ( <. A , B >. Cgr <. C , y >. /\ <. A , x >. Cgr <. C , D >. /\ <. B , x >. Cgr <. y , D >. ) )
86 brcgr3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ x e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ y e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. A , <. B , x >. >. Cgr3 <. C , <. y , D >. >. <-> ( <. A , B >. Cgr <. C , y >. /\ <. A , x >. Cgr <. C , D >. /\ <. B , x >. Cgr <. y , D >. ) ) )
87 21 28 30 31 23 24 26 86 syl133anc 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) -> ( <. A , <. B , x >. >. Cgr3 <. C , <. y , D >. >. <-> ( <. A , B >. Cgr <. C , y >. /\ <. A , x >. Cgr <. C , D >. /\ <. B , x >. Cgr <. y , D >. ) ) )
88 87 3ad2ant1 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) /\ ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) /\ ( <. A , x >. Cgr <. C , D >. /\ <. A , B >. Cgr <. C , y >. /\ <. x , B >. Cgr <. D , y >. ) ) -> ( <. A , <. B , x >. >. Cgr3 <. C , <. y , D >. >. <-> ( <. A , B >. Cgr <. C , y >. /\ <. A , x >. Cgr <. C , D >. /\ <. B , x >. Cgr <. y , D >. ) ) )
89 85 88 mpbird 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) /\ ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) /\ ( <. A , x >. Cgr <. C , D >. /\ <. A , B >. Cgr <. C , y >. /\ <. x , B >. Cgr <. D , y >. ) ) -> <. A , <. B , x >. >. Cgr3 <. C , <. y , D >. >. )
90 btwnxfr 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ x e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ y e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , x >. /\ <. A , <. B , x >. >. Cgr3 <. C , <. y , D >. >. ) -> y Btwn <. C , D >. ) )
91 21 28 30 31 23 24 26 90 syl133anc 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) -> ( ( B Btwn <. A , x >. /\ <. A , <. B , x >. >. Cgr3 <. C , <. y , D >. >. ) -> y Btwn <. C , D >. ) )
92 91 3ad2ant1 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) /\ ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) /\ ( <. A , x >. Cgr <. C , D >. /\ <. A , B >. Cgr <. C , y >. /\ <. x , B >. Cgr <. D , y >. ) ) -> ( ( B Btwn <. A , x >. /\ <. A , <. B , x >. >. Cgr3 <. C , <. y , D >. >. ) -> y Btwn <. C , D >. ) )
93 77 89 92 mp2and 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) /\ ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) /\ ( <. A , x >. Cgr <. C , D >. /\ <. A , B >. Cgr <. C , y >. /\ <. x , B >. Cgr <. D , y >. ) ) -> y Btwn <. C , D >. )
94 93 78 jca 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) /\ ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) /\ ( <. A , x >. Cgr <. C , D >. /\ <. A , B >. Cgr <. C , y >. /\ <. x , B >. Cgr <. D , y >. ) ) -> ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) )
95 94 3expia 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) /\ ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) ) -> ( ( <. A , x >. Cgr <. C , D >. /\ <. A , B >. Cgr <. C , y >. /\ <. x , B >. Cgr <. D , y >. ) -> ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) )
96 76 95 sylbid 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ y e. ( EE ` N ) ) /\ ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) ) -> ( <. A , <. x , B >. >. Cgr3 <. C , <. D , y >. >. -> ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) )
97 96 an32s 
 |-  ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) ) /\ y e. ( EE ` N ) ) -> ( <. A , <. x , B >. >. Cgr3 <. C , <. D , y >. >. -> ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) )
98 97 reximdva 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) ) -> ( E. y e. ( EE ` N ) <. A , <. x , B >. >. Cgr3 <. C , <. D , y >. >. -> E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) )
99 71 98 mpd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) ) -> E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) )
100 99 rexlimdva2 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( E. x e. ( EE ` N ) ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) -> E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) )
101 55 100 impbid 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) <-> E. x e. ( EE ` N ) ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) ) )
102 1 101 bitrd 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. A , B >. Seg<_ <. C , D >. <-> E. x e. ( EE ` N ) ( B Btwn <. A , x >. /\ <. A , x >. Cgr <. C , D >. ) ) )