Metamath Proof Explorer

Theorem ifscgr

Description: Inner five segment congruence. Take two triangles, A D C and E H G , with B between A and C and F between E and G . If the other components of the triangles are congruent, then so are B D and F H . Theorem 4.2 of Schwabhauser p. 34. (Contributed by Scott Fenton, 27-Sep-2013)

Ref Expression
Assertion ifscgr 
|- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. <. A , B >. , <. C , D >. >. InnerFiveSeg <. <. E , F >. , <. G , H >. >. -> <. B , D >. Cgr <. F , H >. ) )

Proof

Step Hyp Ref Expression
1 brifs 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. <. A , B >. , <. C , D >. >. InnerFiveSeg <. <. E , F >. , <. G , H >. >. <-> ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) )
2 simp1l 
 |-  ( ( ( B Btwn <. C , C >. /\ F Btwn <. E , G >. ) /\ ( <. C , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) -> B Btwn <. C , C >. )
3 simp11 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> N e. NN )
4 simp13 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
5 simp21 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
6 axbtwnid 
 |-  ( ( N e. NN /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( B Btwn <. C , C >. -> B = C ) )
7 3 4 5 6 syl3anc 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( B Btwn <. C , C >. -> B = C ) )
8 2 7 syl5 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( ( B Btwn <. C , C >. /\ F Btwn <. E , G >. ) /\ ( <. C , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) -> B = C ) )
9 simp2r 
 |-  ( ( ( B Btwn <. C , C >. /\ F Btwn <. E , G >. ) /\ ( <. C , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) -> <. B , C >. Cgr <. F , G >. )
10 simp3r 
 |-  ( ( ( B Btwn <. C , C >. /\ F Btwn <. E , G >. ) /\ ( <. C , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) -> <. C , D >. Cgr <. G , H >. )
11 9 10 jca 
 |-  ( ( ( B Btwn <. C , C >. /\ F Btwn <. E , G >. ) /\ ( <. C , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) -> ( <. B , C >. Cgr <. F , G >. /\ <. C , D >. Cgr <. G , H >. ) )
12 opeq2 
 |-  ( B = C -> <. B , B >. = <. B , C >. )
13 12 breq1d 
 |-  ( B = C -> ( <. B , B >. Cgr <. F , G >. <-> <. B , C >. Cgr <. F , G >. ) )
14 opeq1 
 |-  ( B = C -> <. B , D >. = <. C , D >. )
15 14 breq1d 
 |-  ( B = C -> ( <. B , D >. Cgr <. G , H >. <-> <. C , D >. Cgr <. G , H >. ) )
16 13 15 anbi12d 
 |-  ( B = C -> ( ( <. B , B >. Cgr <. F , G >. /\ <. B , D >. Cgr <. G , H >. ) <-> ( <. B , C >. Cgr <. F , G >. /\ <. C , D >. Cgr <. G , H >. ) ) )
17 16 biimprd 
 |-  ( B = C -> ( ( <. B , C >. Cgr <. F , G >. /\ <. C , D >. Cgr <. G , H >. ) -> ( <. B , B >. Cgr <. F , G >. /\ <. B , D >. Cgr <. G , H >. ) ) )
18 11 17 mpan9 
 |-  ( ( ( ( B Btwn <. C , C >. /\ F Btwn <. E , G >. ) /\ ( <. C , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) /\ B = C ) -> ( <. B , B >. Cgr <. F , G >. /\ <. B , D >. Cgr <. G , H >. ) )
19 simp31 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> F e. ( EE ` N ) )
20 simp32 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> G e. ( EE ` N ) )
21 cgrid2 
 |-  ( ( N e. NN /\ ( B e. ( EE ` N ) /\ F e. ( EE ` N ) /\ G e. ( EE ` N ) ) ) -> ( <. B , B >. Cgr <. F , G >. -> F = G ) )
22 3 4 19 20 21 syl13anc 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. B , B >. Cgr <. F , G >. -> F = G ) )
23 opeq1 
 |-  ( F = G -> <. F , H >. = <. G , H >. )
24 23 breq2d 
 |-  ( F = G -> ( <. B , D >. Cgr <. F , H >. <-> <. B , D >. Cgr <. G , H >. ) )
25 24 biimprd 
 |-  ( F = G -> ( <. B , D >. Cgr <. G , H >. -> <. B , D >. Cgr <. F , H >. ) )
26 22 25 syl6 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. B , B >. Cgr <. F , G >. -> ( <. B , D >. Cgr <. G , H >. -> <. B , D >. Cgr <. F , H >. ) ) )
27 26 impd 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( <. B , B >. Cgr <. F , G >. /\ <. B , D >. Cgr <. G , H >. ) -> <. B , D >. Cgr <. F , H >. ) )
28 18 27 syl5 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( ( ( B Btwn <. C , C >. /\ F Btwn <. E , G >. ) /\ ( <. C , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) /\ B = C ) -> <. B , D >. Cgr <. F , H >. ) )
29 28 expd 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( ( B Btwn <. C , C >. /\ F Btwn <. E , G >. ) /\ ( <. C , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) -> ( B = C -> <. B , D >. Cgr <. F , H >. ) ) )
30 8 29 mpdd 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( ( B Btwn <. C , C >. /\ F Btwn <. E , G >. ) /\ ( <. C , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) -> <. B , D >. Cgr <. F , H >. ) )
31 opeq1 
 |-  ( A = C -> <. A , C >. = <. C , C >. )
32 31 breq2d 
 |-  ( A = C -> ( B Btwn <. A , C >. <-> B Btwn <. C , C >. ) )
33 32 anbi1d 
 |-  ( A = C -> ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) <-> ( B Btwn <. C , C >. /\ F Btwn <. E , G >. ) ) )
34 31 breq1d 
 |-  ( A = C -> ( <. A , C >. Cgr <. E , G >. <-> <. C , C >. Cgr <. E , G >. ) )
35 34 anbi1d 
 |-  ( A = C -> ( ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) <-> ( <. C , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) ) )
36 33 35 3anbi12d 
 |-  ( A = C -> ( ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) <-> ( ( B Btwn <. C , C >. /\ F Btwn <. E , G >. ) /\ ( <. C , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) )
37 36 imbi1d 
 |-  ( A = C -> ( ( ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) -> <. B , D >. Cgr <. F , H >. ) <-> ( ( ( B Btwn <. C , C >. /\ F Btwn <. E , G >. ) /\ ( <. C , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) -> <. B , D >. Cgr <. F , H >. ) ) )
38 30 37 imbitrrid 
 |-  ( A = C -> ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) -> <. B , D >. Cgr <. F , H >. ) ) )
39 simp12 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
40 btwndiff 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> E. e e. ( EE ` N ) ( C Btwn <. A , e >. /\ C =/= e ) )
41 3 39 5 40 syl3anc 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> E. e e. ( EE ` N ) ( C Btwn <. A , e >. /\ C =/= e ) )
42 simpl11 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ e e. ( EE ` N ) ) -> N e. NN )
43 simpl23 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ e e. ( EE ` N ) ) -> E e. ( EE ` N ) )
44 simpl32 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ e e. ( EE ` N ) ) -> G e. ( EE ` N ) )
45 simpl21 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ e e. ( EE ` N ) ) -> C e. ( EE ` N ) )
46 simpr 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ e e. ( EE ` N ) ) -> e e. ( EE ` N ) )
47 axsegcon 
 |-  ( ( N e. NN /\ ( E e. ( EE ` N ) /\ G e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ e e. ( EE ` N ) ) ) -> E. f e. ( EE ` N ) ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) )
48 42 43 44 45 46 47 syl122anc 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ e e. ( EE ` N ) ) -> E. f e. ( EE ` N ) ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) )
49 anass 
 |-  ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) /\ A =/= C ) ) <-> ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( ( C Btwn <. A , e >. /\ C =/= e ) /\ ( ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) /\ A =/= C ) ) ) )
50 anass 
 |-  ( ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ A =/= C ) <-> ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) /\ A =/= C ) ) )
51 simplrl 
 |-  ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) -> C Btwn <. A , e >. )
52 51 adantl 
 |-  ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) ) -> C Btwn <. A , e >. )
53 simplll 
 |-  ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) -> G Btwn <. E , f >. )
54 53 adantl 
 |-  ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) ) -> G Btwn <. E , f >. )
55 52 54 jca 
 |-  ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) ) -> ( C Btwn <. A , e >. /\ G Btwn <. E , f >. ) )
56 simpr2l 
 |-  ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) -> <. A , C >. Cgr <. E , G >. )
57 56 adantl 
 |-  ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) ) -> <. A , C >. Cgr <. E , G >. )
58 simpllr 
 |-  ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) -> <. G , f >. Cgr <. C , e >. )
59 58 adantl 
 |-  ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) ) -> <. G , f >. Cgr <. C , e >. )
60 3 ad2antrr 
 |-  ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) ) -> N e. NN )
61 20 ad2antrr 
 |-  ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) ) -> G e. ( EE ` N ) )
62 simplrr 
 |-  ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) ) -> f e. ( EE ` N ) )
63 5 ad2antrr 
 |-  ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) ) -> C e. ( EE ` N ) )
64 simplrl 
 |-  ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) ) -> e e. ( EE ` N ) )
65 cgrcom 
 |-  ( ( N e. NN /\ ( G e. ( EE ` N ) /\ f e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ e e. ( EE ` N ) ) ) -> ( <. G , f >. Cgr <. C , e >. <-> <. C , e >. Cgr <. G , f >. ) )
66 60 61 62 63 64 65 syl122anc 
 |-  ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) ) -> ( <. G , f >. Cgr <. C , e >. <-> <. C , e >. Cgr <. G , f >. ) )
67 59 66 mpbid 
 |-  ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) ) -> <. C , e >. Cgr <. G , f >. )
68 57 67 jca 
 |-  ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) ) -> ( <. A , C >. Cgr <. E , G >. /\ <. C , e >. Cgr <. G , f >. ) )
69 simprr3 
 |-  ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) ) -> ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) )
70 55 68 69 3jca 
 |-  ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) ) -> ( ( C Btwn <. A , e >. /\ G Btwn <. E , f >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. C , e >. Cgr <. G , f >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) )
71 70 ex 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) -> ( ( C Btwn <. A , e >. /\ G Btwn <. E , f >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. C , e >. Cgr <. G , f >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) )
72 simpl11 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> N e. NN )
73 simpl12 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
74 simpl21 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
75 simprl 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> e e. ( EE ` N ) )
76 simpl22 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> D e. ( EE ` N ) )
77 simpl23 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> E e. ( EE ` N ) )
78 simpl32 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> G e. ( EE ` N ) )
79 simprr 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> f e. ( EE ` N ) )
80 simpl33 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> H e. ( EE ` N ) )
81 brofs 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( e e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( G e. ( EE ` N ) /\ f e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. <. A , C >. , <. e , D >. >. OuterFiveSeg <. <. E , G >. , <. f , H >. >. <-> ( ( C Btwn <. A , e >. /\ G Btwn <. E , f >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. C , e >. Cgr <. G , f >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) )
82 72 73 74 75 76 77 78 79 80 81 syl333anc 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( <. <. A , C >. , <. e , D >. >. OuterFiveSeg <. <. E , G >. , <. f , H >. >. <-> ( ( C Btwn <. A , e >. /\ G Btwn <. E , f >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. C , e >. Cgr <. G , f >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) )
83 71 82 sylibrd 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) -> <. <. A , C >. , <. e , D >. >. OuterFiveSeg <. <. E , G >. , <. f , H >. >. ) )
84 5segofs 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( e e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( G e. ( EE ` N ) /\ f e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( <. <. A , C >. , <. e , D >. >. OuterFiveSeg <. <. E , G >. , <. f , H >. >. /\ A =/= C ) -> <. e , D >. Cgr <. f , H >. ) )
85 72 73 74 75 76 77 78 79 80 84 syl333anc 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( <. <. A , C >. , <. e , D >. >. OuterFiveSeg <. <. E , G >. , <. f , H >. >. /\ A =/= C ) -> <. e , D >. Cgr <. f , H >. ) )
86 83 85 syland 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ A =/= C ) -> <. e , D >. Cgr <. f , H >. ) )
87 simpr1l 
 |-  ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) -> B Btwn <. A , C >. )
88 87 adantr 
 |-  ( ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ <. e , D >. Cgr <. f , H >. ) -> B Btwn <. A , C >. )
89 51 adantr 
 |-  ( ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ <. e , D >. Cgr <. f , H >. ) -> C Btwn <. A , e >. )
90 88 89 jca 
 |-  ( ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ <. e , D >. Cgr <. f , H >. ) -> ( B Btwn <. A , C >. /\ C Btwn <. A , e >. ) )
91 simpr1r 
 |-  ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) -> F Btwn <. E , G >. )
92 91 adantr 
 |-  ( ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ <. e , D >. Cgr <. f , H >. ) -> F Btwn <. E , G >. )
93 53 adantr 
 |-  ( ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ <. e , D >. Cgr <. f , H >. ) -> G Btwn <. E , f >. )
94 90 92 93 jca32 
 |-  ( ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ <. e , D >. Cgr <. f , H >. ) -> ( ( B Btwn <. A , C >. /\ C Btwn <. A , e >. ) /\ ( F Btwn <. E , G >. /\ G Btwn <. E , f >. ) ) )
95 simpl13 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
96 btwnexch3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ e e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , C >. /\ C Btwn <. A , e >. ) -> C Btwn <. B , e >. ) )
97 72 73 95 74 75 96 syl122anc 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , C >. /\ C Btwn <. A , e >. ) -> C Btwn <. B , e >. ) )
98 simpl31 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> F e. ( EE ` N ) )
99 btwnexch3 
 |-  ( ( N e. NN /\ ( E e. ( EE ` N ) /\ F e. ( EE ` N ) ) /\ ( G e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( F Btwn <. E , G >. /\ G Btwn <. E , f >. ) -> G Btwn <. F , f >. ) )
100 72 77 98 78 79 99 syl122anc 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( F Btwn <. E , G >. /\ G Btwn <. E , f >. ) -> G Btwn <. F , f >. ) )
101 97 100 anim12d 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( ( B Btwn <. A , C >. /\ C Btwn <. A , e >. ) /\ ( F Btwn <. E , G >. /\ G Btwn <. E , f >. ) ) -> ( C Btwn <. B , e >. /\ G Btwn <. F , f >. ) ) )
102 94 101 syl5 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ <. e , D >. Cgr <. f , H >. ) -> ( C Btwn <. B , e >. /\ G Btwn <. F , f >. ) ) )
103 102 imp 
 |-  ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ <. e , D >. Cgr <. f , H >. ) ) -> ( C Btwn <. B , e >. /\ G Btwn <. F , f >. ) )
104 btwncom 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ B e. ( EE ` N ) /\ e e. ( EE ` N ) ) ) -> ( C Btwn <. B , e >. <-> C Btwn <. e , B >. ) )
105 72 74 95 75 104 syl13anc 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( C Btwn <. B , e >. <-> C Btwn <. e , B >. ) )
106 btwncom 
 |-  ( ( N e. NN /\ ( G e. ( EE ` N ) /\ F e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( G Btwn <. F , f >. <-> G Btwn <. f , F >. ) )
107 72 78 98 79 106 syl13anc 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( G Btwn <. F , f >. <-> G Btwn <. f , F >. ) )
108 105 107 anbi12d 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( C Btwn <. B , e >. /\ G Btwn <. F , f >. ) <-> ( C Btwn <. e , B >. /\ G Btwn <. f , F >. ) ) )
109 108 adantr 
 |-  ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ <. e , D >. Cgr <. f , H >. ) ) -> ( ( C Btwn <. B , e >. /\ G Btwn <. F , f >. ) <-> ( C Btwn <. e , B >. /\ G Btwn <. f , F >. ) ) )
110 103 109 mpbid 
 |-  ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ <. e , D >. Cgr <. f , H >. ) ) -> ( C Btwn <. e , B >. /\ G Btwn <. f , F >. ) )
111 58 ad2antrl 
 |-  ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ <. e , D >. Cgr <. f , H >. ) ) -> <. G , f >. Cgr <. C , e >. )
112 72 78 79 74 75 65 syl122anc 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( <. G , f >. Cgr <. C , e >. <-> <. C , e >. Cgr <. G , f >. ) )
113 cgrcomlr 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ e e. ( EE ` N ) ) /\ ( G e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( <. C , e >. Cgr <. G , f >. <-> <. e , C >. Cgr <. f , G >. ) )
114 72 74 75 78 79 113 syl122anc 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( <. C , e >. Cgr <. G , f >. <-> <. e , C >. Cgr <. f , G >. ) )
115 112 114 bitrd 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( <. G , f >. Cgr <. C , e >. <-> <. e , C >. Cgr <. f , G >. ) )
116 115 adantr 
 |-  ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ <. e , D >. Cgr <. f , H >. ) ) -> ( <. G , f >. Cgr <. C , e >. <-> <. e , C >. Cgr <. f , G >. ) )
117 111 116 mpbid 
 |-  ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ <. e , D >. Cgr <. f , H >. ) ) -> <. e , C >. Cgr <. f , G >. )
118 simpr2r 
 |-  ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) -> <. B , C >. Cgr <. F , G >. )
119 118 ad2antrl 
 |-  ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ <. e , D >. Cgr <. f , H >. ) ) -> <. B , C >. Cgr <. F , G >. )
120 72 95 74 98 78 119 cgrcomlrand 
 |-  ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ <. e , D >. Cgr <. f , H >. ) ) -> <. C , B >. Cgr <. G , F >. )
121 117 120 jca 
 |-  ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ <. e , D >. Cgr <. f , H >. ) ) -> ( <. e , C >. Cgr <. f , G >. /\ <. C , B >. Cgr <. G , F >. ) )
122 simprr 
 |-  ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ <. e , D >. Cgr <. f , H >. ) ) -> <. e , D >. Cgr <. f , H >. )
123 simpr3r 
 |-  ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) -> <. C , D >. Cgr <. G , H >. )
124 123 ad2antrl 
 |-  ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ <. e , D >. Cgr <. f , H >. ) ) -> <. C , D >. Cgr <. G , H >. )
125 122 124 jca 
 |-  ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ <. e , D >. Cgr <. f , H >. ) ) -> ( <. e , D >. Cgr <. f , H >. /\ <. C , D >. Cgr <. G , H >. ) )
126 110 121 125 3jca 
 |-  ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) /\ ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ <. e , D >. Cgr <. f , H >. ) ) -> ( ( C Btwn <. e , B >. /\ G Btwn <. f , F >. ) /\ ( <. e , C >. Cgr <. f , G >. /\ <. C , B >. Cgr <. G , F >. ) /\ ( <. e , D >. Cgr <. f , H >. /\ <. C , D >. Cgr <. G , H >. ) ) )
127 126 ex 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ <. e , D >. Cgr <. f , H >. ) -> ( ( C Btwn <. e , B >. /\ G Btwn <. f , F >. ) /\ ( <. e , C >. Cgr <. f , G >. /\ <. C , B >. Cgr <. G , F >. ) /\ ( <. e , D >. Cgr <. f , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) )
128 brofs 
 |-  ( ( ( N e. NN /\ e e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ D e. ( EE ` N ) /\ f e. ( EE ` N ) ) /\ ( G e. ( EE ` N ) /\ F e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. <. e , C >. , <. B , D >. >. OuterFiveSeg <. <. f , G >. , <. F , H >. >. <-> ( ( C Btwn <. e , B >. /\ G Btwn <. f , F >. ) /\ ( <. e , C >. Cgr <. f , G >. /\ <. C , B >. Cgr <. G , F >. ) /\ ( <. e , D >. Cgr <. f , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) )
129 72 75 74 95 76 79 78 98 80 128 syl333anc 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( <. <. e , C >. , <. B , D >. >. OuterFiveSeg <. <. f , G >. , <. F , H >. >. <-> ( ( C Btwn <. e , B >. /\ G Btwn <. f , F >. ) /\ ( <. e , C >. Cgr <. f , G >. /\ <. C , B >. Cgr <. G , F >. ) /\ ( <. e , D >. Cgr <. f , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) )
130 127 129 sylibrd 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ <. e , D >. Cgr <. f , H >. ) -> <. <. e , C >. , <. B , D >. >. OuterFiveSeg <. <. f , G >. , <. F , H >. >. ) )
131 simplrr 
 |-  ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) -> C =/= e )
132 131 adantr 
 |-  ( ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ <. e , D >. Cgr <. f , H >. ) -> C =/= e )
133 132 necomd 
 |-  ( ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ <. e , D >. Cgr <. f , H >. ) -> e =/= C )
134 133 a1i 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ <. e , D >. Cgr <. f , H >. ) -> e =/= C ) )
135 130 134 jcad 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ <. e , D >. Cgr <. f , H >. ) -> ( <. <. e , C >. , <. B , D >. >. OuterFiveSeg <. <. f , G >. , <. F , H >. >. /\ e =/= C ) ) )
136 5segofs 
 |-  ( ( ( N e. NN /\ e e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ D e. ( EE ` N ) /\ f e. ( EE ` N ) ) /\ ( G e. ( EE ` N ) /\ F e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( <. <. e , C >. , <. B , D >. >. OuterFiveSeg <. <. f , G >. , <. F , H >. >. /\ e =/= C ) -> <. B , D >. Cgr <. F , H >. ) )
137 72 75 74 95 76 79 78 98 80 136 syl333anc 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( <. <. e , C >. , <. B , D >. >. OuterFiveSeg <. <. f , G >. , <. F , H >. >. /\ e =/= C ) -> <. B , D >. Cgr <. F , H >. ) )
138 135 137 syld 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ <. e , D >. Cgr <. f , H >. ) -> <. B , D >. Cgr <. F , H >. ) )
139 138 expd 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) -> ( <. e , D >. Cgr <. f , H >. -> <. B , D >. Cgr <. F , H >. ) ) )
140 139 adantrd 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ A =/= C ) -> ( <. e , D >. Cgr <. f , H >. -> <. B , D >. Cgr <. F , H >. ) ) )
141 86 140 mpdd 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) /\ A =/= C ) -> <. B , D >. Cgr <. F , H >. ) )
142 50 141 biimtrrid 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( C Btwn <. A , e >. /\ C =/= e ) ) /\ ( ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) /\ A =/= C ) ) -> <. B , D >. Cgr <. F , H >. ) )
143 49 142 biimtrrid 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) /\ ( ( C Btwn <. A , e >. /\ C =/= e ) /\ ( ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) /\ A =/= C ) ) ) -> <. B , D >. Cgr <. F , H >. ) )
144 143 expd 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ ( e e. ( EE ` N ) /\ f e. ( EE ` N ) ) ) -> ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) -> ( ( ( C Btwn <. A , e >. /\ C =/= e ) /\ ( ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) /\ A =/= C ) ) -> <. B , D >. Cgr <. F , H >. ) ) )
145 144 anassrs 
 |-  ( ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ e e. ( EE ` N ) ) /\ f e. ( EE ` N ) ) -> ( ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) -> ( ( ( C Btwn <. A , e >. /\ C =/= e ) /\ ( ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) /\ A =/= C ) ) -> <. B , D >. Cgr <. F , H >. ) ) )
146 145 rexlimdva 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ e e. ( EE ` N ) ) -> ( E. f e. ( EE ` N ) ( G Btwn <. E , f >. /\ <. G , f >. Cgr <. C , e >. ) -> ( ( ( C Btwn <. A , e >. /\ C =/= e ) /\ ( ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) /\ A =/= C ) ) -> <. B , D >. Cgr <. F , H >. ) ) )
147 48 146 mpd 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ e e. ( EE ` N ) ) -> ( ( ( C Btwn <. A , e >. /\ C =/= e ) /\ ( ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) /\ A =/= C ) ) -> <. B , D >. Cgr <. F , H >. ) )
148 147 expd 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) /\ e e. ( EE ` N ) ) -> ( ( C Btwn <. A , e >. /\ C =/= e ) -> ( ( ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) /\ A =/= C ) -> <. B , D >. Cgr <. F , H >. ) ) )
149 148 rexlimdva 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( E. e e. ( EE ` N ) ( C Btwn <. A , e >. /\ C =/= e ) -> ( ( ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) /\ A =/= C ) -> <. B , D >. Cgr <. F , H >. ) ) )
150 41 149 mpd 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) /\ A =/= C ) -> <. B , D >. Cgr <. F , H >. ) )
151 150 expd 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) -> ( A =/= C -> <. B , D >. Cgr <. F , H >. ) ) )
152 151 com3r 
 |-  ( A =/= C -> ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) -> <. B , D >. Cgr <. F , H >. ) ) )
153 38 152 pm2.61ine 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) -> <. B , D >. Cgr <. F , H >. ) )
154 1 153 sylbid 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. <. A , B >. , <. C , D >. >. InnerFiveSeg <. <. E , F >. , <. G , H >. >. -> <. B , D >. Cgr <. F , H >. ) )