Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ifscgr Unicode version

Theorem ifscgr 24739
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.)
Assertion
Ref Expression
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 of Theorem ifscgr
Dummy variables  e 
f are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 brifs 24738 . 2  |-  ( ( ( 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 979 . . . . . 6  |-  ( ( ( 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 985 . . . . . . 7  |-  ( ( ( 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 987 . . . . . . 7  |-  ( ( ( 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 988 . . . . . . 7  |-  ( ( ( 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 24639 . . . . . . 7  |-  ( ( N  e.  NN  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  ( B  Btwn  <. C ,  C >.  ->  B  =  C ) )
73, 4, 5, 6syl3anc 1182 . . . . . 6  |-  ( ( ( 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 ) )
82, 7syl5 28 . . . . 5  |-  ( ( ( 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 982 . . . . . . . . 9  |-  ( ( ( 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 984 . . . . . . . . 9  |-  ( ( ( 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 >. )
119, 10jca 518 . . . . . . . 8  |-  ( ( ( 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 3813 . . . . . . . . . . 11  |-  ( B  =  C  ->  <. B ,  B >.  =  <. B ,  C >. )
1312breq1d 4049 . . . . . . . . . 10  |-  ( B  =  C  ->  ( <. B ,  B >.Cgr <. F ,  G >.  <->  <. B ,  C >.Cgr <. F ,  G >. ) )
14 opeq1 3812 . . . . . . . . . . 11  |-  ( B  =  C  ->  <. B ,  D >.  =  <. C ,  D >. )
1514breq1d 4049 . . . . . . . . . 10  |-  ( B  =  C  ->  ( <. B ,  D >.Cgr <. G ,  H >.  <->  <. C ,  D >.Cgr <. G ,  H >. ) )
1613, 15anbi12d 691 . . . . . . . . 9  |-  ( B  =  C  ->  (
( <. B ,  B >.Cgr
<. F ,  G >.  /\ 
<. B ,  D >.Cgr <. G ,  H >. )  <-> 
( <. B ,  C >.Cgr
<. F ,  G >.  /\ 
<. C ,  D >.Cgr <. G ,  H >. ) ) )
1716biimprd 214 . . . . . . . 8  |-  ( B  =  C  ->  (
( <. B ,  C >.Cgr
<. F ,  G >.  /\ 
<. C ,  D >.Cgr <. G ,  H >. )  ->  ( <. B ,  B >.Cgr <. F ,  G >.  /\  <. B ,  D >.Cgr
<. G ,  H >. ) ) )
1811, 17mpan9 455 . . . . . . 7  |-  ( ( ( ( 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 991 . . . . . . . . . 10  |-  ( ( ( 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 992 . . . . . . . . . 10  |-  ( ( ( 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 24698 . . . . . . . . . 10  |-  ( ( N  e.  NN  /\  ( B  e.  ( EE `  N )  /\  F  e.  ( EE `  N )  /\  G  e.  ( EE `  N
) ) )  -> 
( <. B ,  B >.Cgr
<. F ,  G >.  ->  F  =  G )
)
223, 4, 19, 20, 21syl13anc 1184 . . . . . . . . 9  |-  ( ( ( 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 3812 . . . . . . . . . . 11  |-  ( F  =  G  ->  <. F ,  H >.  =  <. G ,  H >. )
2423breq2d 4051 . . . . . . . . . 10  |-  ( F  =  G  ->  ( <. B ,  D >.Cgr <. F ,  H >.  <->  <. B ,  D >.Cgr <. G ,  H >. ) )
2524biimprd 214 . . . . . . . . 9  |-  ( F  =  G  ->  ( <. B ,  D >.Cgr <. G ,  H >.  ->  <. B ,  D >.Cgr <. F ,  H >. ) )
2622, 25syl6 29 . . . . . . . 8  |-  ( ( ( 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 >. ) ) )
2726imp3a 420 . . . . . . 7  |-  ( ( ( 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 >. ) )
2818, 27syl5 28 . . . . . 6  |-  ( ( ( 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 >. ) )
2928exp3a 425 . . . . 5  |-  ( ( ( 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 >. ) ) )
308, 29mpdd 36 . . . 4  |-  ( ( ( 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 3812 . . . . . . . 8  |-  ( A  =  C  ->  <. A ,  C >.  =  <. C ,  C >. )
3231breq2d 4051 . . . . . . 7  |-  ( A  =  C  ->  ( B  Btwn  <. A ,  C >.  <-> 
B  Btwn  <. C ,  C >. ) )
3332anbi1d 685 . . . . . 6  |-  ( A  =  C  ->  (
( B  Btwn  <. A ,  C >.  /\  F  Btwn  <. E ,  G >. )  <-> 
( B  Btwn  <. C ,  C >.  /\  F  Btwn  <. E ,  G >. ) ) )
3431breq1d 4049 . . . . . . 7  |-  ( A  =  C  ->  ( <. A ,  C >.Cgr <. E ,  G >.  <->  <. C ,  C >.Cgr <. E ,  G >. ) )
3534anbi1d 685 . . . . . 6  |-  ( A  =  C  ->  (
( <. A ,  C >.Cgr
<. E ,  G >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. )  <-> 
( <. C ,  C >.Cgr
<. E ,  G >.  /\ 
<. B ,  C >.Cgr <. F ,  G >. ) ) )
3633, 353anbi12d 1253 . . . . 5  |-  ( 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 >. ) ) ) )
3736imbi1d 308 . . . 4  |-  ( 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 >. ) ) )
3830, 37syl5ibr 212 . . 3  |-  ( 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 986 . . . . . . 7  |-  ( ( ( 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 24722 . . . . . . 7  |-  ( ( N  e.  NN  /\  A  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  ->  E. e  e.  ( EE `  N
) ( C  Btwn  <. A ,  e >.  /\  C  =/=  e ) )
413, 39, 5, 40syl3anc 1182 . . . . . 6  |-  ( ( ( 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 1030 . . . . . . . . . 10  |-  ( ( ( ( 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 1035 . . . . . . . . . 10  |-  ( ( ( ( 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 1037 . . . . . . . . . 10  |-  ( ( ( ( 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 1033 . . . . . . . . . 10  |-  ( ( ( ( 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 447 . . . . . . . . . 10  |-  ( ( ( ( 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 24627 . . . . . . . . . 10  |-  ( ( 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
>. ) )
4842, 43, 44, 45, 46, 47syl122anc 1191 . . . . . . . . 9  |-  ( ( ( ( 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 630 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 630 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( 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 736 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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
>. )
5251adantl 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( 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 734 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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
>. )
5453adantl 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( 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
>. )
5552, 54jca 518 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( 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 1014 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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 >. )
5756adantl 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( 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 735 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 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
>. )
5958adantl 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( 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 >.
)
603ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( 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 )
6120ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( 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 737 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( 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 ) )
635ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( 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 736 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( 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 24685 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 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 >.
) )
6660, 61, 62, 63, 64, 65syl122anc 1191 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( 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 >.
) )
6759, 66mpbid 201 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( 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 >.
)
6857, 67jca 518 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( 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 1005 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( 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 >. ) )
7055, 68, 693jca 1132 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( 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 >. ) ) )
7170ex 423 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 1030 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 1031 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 1033 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 732 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 1034 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 1035 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 1037 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 733 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 1038 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 24700 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 >. ) ) ) )
8272, 73, 74, 75, 76, 77, 78, 79, 80, 81syl333anc 1214 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 >. ) ) ) )
8371, 82sylibrd 225 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 24701 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 >. ) )
8572, 73, 74, 75, 76, 77, 78, 79, 80, 84syl333anc 1214 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 >. ) )
8683, 85syland 467 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 1012 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( 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 >. )
8887adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( 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 >. )
8951adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( 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
>. )
9088, 89jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( 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 1013 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( 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 >. )
9291adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( 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 >. )
9353adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( 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
>. )
9490, 92, 93jca32 521 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( 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 1032 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( 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 24715 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( 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
>. ) )
9772, 73, 95, 74, 75, 96syl122anc 1191 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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 1036 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( 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 24715 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( 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
>. ) )
10072, 77, 98, 78, 79, 99syl122anc 1191 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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
>. ) )
10197, 100anim12d 546 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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 >. ) ) )
10294, 101syl5 28 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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 >. ) ) )
103102imp 418 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( 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 24709 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( N  e.  NN  /\  ( C  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  e  e.  ( EE `  N
) ) )  -> 
( C  Btwn  <. B , 
e >. 
<->  C  Btwn  <. e ,  B >. ) )
10572, 74, 95, 75, 104syl13anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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 24709 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( N  e.  NN  /\  ( G  e.  ( EE `  N )  /\  F  e.  ( EE `  N )  /\  f  e.  ( EE `  N
) ) )  -> 
( G  Btwn  <. F , 
f >. 
<->  G  Btwn  <. f ,  F >. ) )
10772, 78, 98, 79, 106syl13anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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 >. ) )
108105, 107anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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 >. ) ) )
109108adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( 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 >. ) ) )
110103, 109mpbid 201 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( 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 >. ) )
11158ad2antrl 708 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( 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 >.
)
11272, 78, 79, 74, 75, 65syl122anc 1191 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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 24693 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( 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 >. ) )
11472, 74, 75, 78, 79, 113syl122anc 1191 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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 >. ) )
115112, 114bitrd 244 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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 >. ) )
116115adantr 451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( 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 >. ) )
117111, 116mpbid 201 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( 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 1015 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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 >. )
119118ad2antrl 708 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( 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 >. )
12072, 95, 74, 98, 78, 119cgrcomlrand 24696 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( 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 >. )
121117, 120jca 518 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( 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 733 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( 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 1017 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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 >. )
124123ad2antrl 708 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( 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 >. )
125122, 124jca 518 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( 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 >. ) ) )  /\