Metamath Proof Explorer

Theorem brifs2

Description: Change some conditions for inner five segment predicate. (Contributed by Scott Fenton, 6-Oct-2013)

Ref Expression
Assertion brifs2 
|- ( ( ( 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 >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , 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 simpr1l 
 |-  ( ( ( ( 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 Btwn <. A , C >. )
3 3simpa 
 |-  ( ( ( 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 >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) ) )
4 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 )
5 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 ) )
6 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 ) )
7 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 ) )
8 simp23 
 |-  ( ( ( 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 ) )
9 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 ) )
10 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 ) )
11 cgrsub 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ F e. ( EE ` N ) /\ G e. ( EE ` N ) ) ) -> ( ( ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) /\ ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) ) -> <. A , B >. Cgr <. E , F >. ) )
12 4 5 6 7 8 9 10 11 syl133anc 
 |-  ( ( ( 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 , B >. Cgr <. E , F >. ) )
13 3 12 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 <. 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 , B >. Cgr <. E , F >. ) )
14 13 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 ) ) ) /\ ( ( 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 , B >. Cgr <. E , F >. )
15 simpr2l 
 |-  ( ( ( ( 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 >. Cgr <. E , G >. )
16 simpr2r 
 |-  ( ( ( ( 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 , C >. Cgr <. F , G >. )
17 14 15 16 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 ) ) ) /\ ( ( 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 , B >. Cgr <. E , F >. /\ <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) )
18 17 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 ) ) ) -> ( ( ( 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 , B >. Cgr <. E , F >. /\ <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) ) )
19 brcgr3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ F e. ( EE ` N ) /\ G e. ( EE ` N ) ) ) -> ( <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. <-> ( <. A , B >. Cgr <. E , F >. /\ <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) ) )
20 4 5 6 7 8 9 10 19 syl133anc 
 |-  ( ( ( 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 >. >. Cgr3 <. E , <. F , G >. >. <-> ( <. A , B >. Cgr <. E , F >. /\ <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) ) )
21 18 20 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 ) ) ) -> ( ( ( 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 , <. B , C >. >. Cgr3 <. E , <. F , G >. >. ) )
22 21 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 ) ) ) /\ ( ( 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 , <. B , C >. >. Cgr3 <. E , <. F , G >. >. )
23 simpr3 
 |-  ( ( ( ( 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 , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) )
24 2 22 23 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 ) ) ) /\ ( ( 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 >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) )
25 simpr1 
 |-  ( ( ( ( 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 >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) -> B Btwn <. A , C >. )
26 3simpa 
 |-  ( ( B Btwn <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) -> ( B Btwn <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. ) )
27 btwnxfr 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ F e. ( EE ` N ) /\ G e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. ) -> F Btwn <. E , G >. ) )
28 4 5 6 7 8 9 10 27 syl133anc 
 |-  ( ( ( 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 >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. ) -> F Btwn <. E , G >. ) )
29 26 28 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 <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) -> F Btwn <. E , G >. ) )
30 29 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 ) ) ) /\ ( B Btwn <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) -> F Btwn <. E , G >. )
31 25 30 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 ) ) ) /\ ( B Btwn <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) -> ( B Btwn <. A , C >. /\ F Btwn <. E , G >. ) )
32 3simpc 
 |-  ( ( <. A , B >. Cgr <. E , F >. /\ <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) -> ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) )
33 20 32 syl6bi 
 |-  ( ( ( 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 >. >. Cgr3 <. E , <. F , G >. >. -> ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) ) )
34 33 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 ) ) ) /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. ) -> ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) )
35 34 3ad2antr2 
 |-  ( ( ( ( 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 >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) -> ( <. A , C >. Cgr <. E , G >. /\ <. B , C >. Cgr <. F , G >. ) )
36 simpr3 
 |-  ( ( ( ( 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 >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) -> ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) )
37 31 35 36 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 ) ) ) /\ ( B Btwn <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. 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 >. ) ) )
38 24 37 impbida 
 |-  ( ( ( 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 Btwn <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) )
39 1 38 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 ) ) ) -> ( <. <. A , B >. , <. C , D >. >. InnerFiveSeg <. <. E , F >. , <. G , H >. >. <-> ( B Btwn <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. C , D >. Cgr <. G , H >. ) ) ) )