Metamath Proof Explorer

Theorem usgrexmpl2trifr

Description: G is triangle-free. (Contributed by AV, 10-Aug-2025)

Ref Expression
Hypotheses usgrexmpl2.v 
|- V = ( 0 ... 5 )
usgrexmpl2.e 
|- E = <" { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } ">
usgrexmpl2.g 
|- G = <. V , E >.
Assertion usgrexmpl2trifr 
|- -. E. t t e. ( GrTriangles ` G )

Proof

Step Hyp Ref Expression
1 usgrexmpl2.v 
 |-  V = ( 0 ... 5 )
2 usgrexmpl2.e 
 |-  E = <" { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } ">
3 usgrexmpl2.g 
 |-  G = <. V , E >.
4 1 2 3 usgrexmpl2nb0 
 |-  ( G NeighbVtx 0 ) = { 1 , 3 , 5 }
5 4 eleq2i 
 |-  ( b e. ( G NeighbVtx 0 ) <-> b e. { 1 , 3 , 5 } )
6 vex 
 |-  b e. _V
7 6 eltp 
 |-  ( b e. { 1 , 3 , 5 } <-> ( b = 1 \/ b = 3 \/ b = 5 ) )
8 5 7 bitri 
 |-  ( b e. ( G NeighbVtx 0 ) <-> ( b = 1 \/ b = 3 \/ b = 5 ) )
9 4 eleq2i 
 |-  ( c e. ( G NeighbVtx 0 ) <-> c e. { 1 , 3 , 5 } )
10 vex 
 |-  c e. _V
11 10 eltp 
 |-  ( c e. { 1 , 3 , 5 } <-> ( c = 1 \/ c = 3 \/ c = 5 ) )
12 9 11 bitri 
 |-  ( c e. ( G NeighbVtx 0 ) <-> ( c = 1 \/ c = 3 \/ c = 5 ) )
13 eqtr3 
 |-  ( ( b = 1 /\ c = 1 ) -> b = c )
14 13 orcd 
 |-  ( ( b = 1 /\ c = 1 ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
15 ax-1ne0 
 |-  1 =/= 0
16 neeq1 
 |-  ( b = 1 -> ( b =/= 0 <-> 1 =/= 0 ) )
17 15 16 mpbiri 
 |-  ( b = 1 -> b =/= 0 )
18 17 adantr 
 |-  ( ( b = 1 /\ c = 3 ) -> b =/= 0 )
19 18 neneqd 
 |-  ( ( b = 1 /\ c = 3 ) -> -. b = 0 )
20 19 orcd 
 |-  ( ( b = 1 /\ c = 3 ) -> ( -. b = 0 \/ -. c = 3 ) )
21 3ne0 
 |-  3 =/= 0
22 neeq1 
 |-  ( c = 3 -> ( c =/= 0 <-> 3 =/= 0 ) )
23 21 22 mpbiri 
 |-  ( c = 3 -> c =/= 0 )
24 23 adantl 
 |-  ( ( b = 1 /\ c = 3 ) -> c =/= 0 )
25 24 neneqd 
 |-  ( ( b = 1 /\ c = 3 ) -> -. c = 0 )
26 25 olcd 
 |-  ( ( b = 1 /\ c = 3 ) -> ( -. b = 3 \/ -. c = 0 ) )
27 19 orcd 
 |-  ( ( b = 1 /\ c = 3 ) -> ( -. b = 0 \/ -. c = 1 ) )
28 25 olcd 
 |-  ( ( b = 1 /\ c = 3 ) -> ( -. b = 1 \/ -. c = 0 ) )
29 27 28 jca 
 |-  ( ( b = 1 /\ c = 3 ) -> ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) )
30 2re 
 |-  2 e. RR
31 2lt3 
 |-  2 < 3
32 30 31 gtneii 
 |-  3 =/= 2
33 neeq1 
 |-  ( c = 3 -> ( c =/= 2 <-> 3 =/= 2 ) )
34 32 33 mpbiri 
 |-  ( c = 3 -> c =/= 2 )
35 34 adantl 
 |-  ( ( b = 1 /\ c = 3 ) -> c =/= 2 )
36 35 neneqd 
 |-  ( ( b = 1 /\ c = 3 ) -> -. c = 2 )
37 36 olcd 
 |-  ( ( b = 1 /\ c = 3 ) -> ( -. b = 1 \/ -. c = 2 ) )
38 1re 
 |-  1 e. RR
39 1lt3 
 |-  1 < 3
40 38 39 gtneii 
 |-  3 =/= 1
41 neeq1 
 |-  ( c = 3 -> ( c =/= 1 <-> 3 =/= 1 ) )
42 40 41 mpbiri 
 |-  ( c = 3 -> c =/= 1 )
43 42 adantl 
 |-  ( ( b = 1 /\ c = 3 ) -> c =/= 1 )
44 43 neneqd 
 |-  ( ( b = 1 /\ c = 3 ) -> -. c = 1 )
45 44 olcd 
 |-  ( ( b = 1 /\ c = 3 ) -> ( -. b = 2 \/ -. c = 1 ) )
46 37 45 jca 
 |-  ( ( b = 1 /\ c = 3 ) -> ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) )
47 1ne2 
 |-  1 =/= 2
48 neeq1 
 |-  ( b = 1 -> ( b =/= 2 <-> 1 =/= 2 ) )
49 47 48 mpbiri 
 |-  ( b = 1 -> b =/= 2 )
50 49 adantr 
 |-  ( ( b = 1 /\ c = 3 ) -> b =/= 2 )
51 50 neneqd 
 |-  ( ( b = 1 /\ c = 3 ) -> -. b = 2 )
52 51 orcd 
 |-  ( ( b = 1 /\ c = 3 ) -> ( -. b = 2 \/ -. c = 3 ) )
53 36 olcd 
 |-  ( ( b = 1 /\ c = 3 ) -> ( -. b = 3 \/ -. c = 2 ) )
54 52 53 jca 
 |-  ( ( b = 1 /\ c = 3 ) -> ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) )
55 29 46 54 3jca 
 |-  ( ( b = 1 /\ c = 3 ) -> ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) )
56 38 39 ltneii 
 |-  1 =/= 3
57 neeq1 
 |-  ( b = 1 -> ( b =/= 3 <-> 1 =/= 3 ) )
58 56 57 mpbiri 
 |-  ( b = 1 -> b =/= 3 )
59 58 adantr 
 |-  ( ( b = 1 /\ c = 3 ) -> b =/= 3 )
60 59 neneqd 
 |-  ( ( b = 1 /\ c = 3 ) -> -. b = 3 )
61 60 orcd 
 |-  ( ( b = 1 /\ c = 3 ) -> ( -. b = 3 \/ -. c = 4 ) )
62 1lt4 
 |-  1 < 4
63 38 62 ltneii 
 |-  1 =/= 4
64 neeq1 
 |-  ( b = 1 -> ( b =/= 4 <-> 1 =/= 4 ) )
65 63 64 mpbiri 
 |-  ( b = 1 -> b =/= 4 )
66 65 adantr 
 |-  ( ( b = 1 /\ c = 3 ) -> b =/= 4 )
67 66 neneqd 
 |-  ( ( b = 1 /\ c = 3 ) -> -. b = 4 )
68 67 orcd 
 |-  ( ( b = 1 /\ c = 3 ) -> ( -. b = 4 \/ -. c = 3 ) )
69 61 68 jca 
 |-  ( ( b = 1 /\ c = 3 ) -> ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) )
70 67 orcd 
 |-  ( ( b = 1 /\ c = 3 ) -> ( -. b = 4 \/ -. c = 5 ) )
71 1lt5 
 |-  1 < 5
72 38 71 ltneii 
 |-  1 =/= 5
73 neeq1 
 |-  ( b = 1 -> ( b =/= 5 <-> 1 =/= 5 ) )
74 72 73 mpbiri 
 |-  ( b = 1 -> b =/= 5 )
75 74 adantr 
 |-  ( ( b = 1 /\ c = 3 ) -> b =/= 5 )
76 75 neneqd 
 |-  ( ( b = 1 /\ c = 3 ) -> -. b = 5 )
77 76 orcd 
 |-  ( ( b = 1 /\ c = 3 ) -> ( -. b = 5 \/ -. c = 4 ) )
78 70 77 jca 
 |-  ( ( b = 1 /\ c = 3 ) -> ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) )
79 19 orcd 
 |-  ( ( b = 1 /\ c = 3 ) -> ( -. b = 0 \/ -. c = 5 ) )
80 25 olcd 
 |-  ( ( b = 1 /\ c = 3 ) -> ( -. b = 5 \/ -. c = 0 ) )
81 79 80 jca 
 |-  ( ( b = 1 /\ c = 3 ) -> ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) )
82 69 78 81 3jca 
 |-  ( ( b = 1 /\ c = 3 ) -> ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) )
83 55 82 jca 
 |-  ( ( b = 1 /\ c = 3 ) -> ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) )
84 20 26 83 jca31 
 |-  ( ( b = 1 /\ c = 3 ) -> ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) )
85 84 olcd 
 |-  ( ( b = 1 /\ c = 3 ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
86 17 adantr 
 |-  ( ( b = 1 /\ c = 5 ) -> b =/= 0 )
87 86 neneqd 
 |-  ( ( b = 1 /\ c = 5 ) -> -. b = 0 )
88 87 orcd 
 |-  ( ( b = 1 /\ c = 5 ) -> ( -. b = 0 \/ -. c = 3 ) )
89 58 adantr 
 |-  ( ( b = 1 /\ c = 5 ) -> b =/= 3 )
90 89 neneqd 
 |-  ( ( b = 1 /\ c = 5 ) -> -. b = 3 )
91 90 orcd 
 |-  ( ( b = 1 /\ c = 5 ) -> ( -. b = 3 \/ -. c = 0 ) )
92 87 orcd 
 |-  ( ( b = 1 /\ c = 5 ) -> ( -. b = 0 \/ -. c = 1 ) )
93 0re 
 |-  0 e. RR
94 5pos 
 |-  0 < 5
95 93 94 gtneii 
 |-  5 =/= 0
96 neeq1 
 |-  ( c = 5 -> ( c =/= 0 <-> 5 =/= 0 ) )
97 95 96 mpbiri 
 |-  ( c = 5 -> c =/= 0 )
98 97 adantl 
 |-  ( ( b = 1 /\ c = 5 ) -> c =/= 0 )
99 98 neneqd 
 |-  ( ( b = 1 /\ c = 5 ) -> -. c = 0 )
100 99 olcd 
 |-  ( ( b = 1 /\ c = 5 ) -> ( -. b = 1 \/ -. c = 0 ) )
101 92 100 jca 
 |-  ( ( b = 1 /\ c = 5 ) -> ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) )
102 2lt5 
 |-  2 < 5
103 30 102 gtneii 
 |-  5 =/= 2
104 neeq1 
 |-  ( c = 5 -> ( c =/= 2 <-> 5 =/= 2 ) )
105 103 104 mpbiri 
 |-  ( c = 5 -> c =/= 2 )
106 105 adantl 
 |-  ( ( b = 1 /\ c = 5 ) -> c =/= 2 )
107 106 neneqd 
 |-  ( ( b = 1 /\ c = 5 ) -> -. c = 2 )
108 107 olcd 
 |-  ( ( b = 1 /\ c = 5 ) -> ( -. b = 1 \/ -. c = 2 ) )
109 49 adantr 
 |-  ( ( b = 1 /\ c = 5 ) -> b =/= 2 )
110 109 neneqd 
 |-  ( ( b = 1 /\ c = 5 ) -> -. b = 2 )
111 110 orcd 
 |-  ( ( b = 1 /\ c = 5 ) -> ( -. b = 2 \/ -. c = 1 ) )
112 108 111 jca 
 |-  ( ( b = 1 /\ c = 5 ) -> ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) )
113 110 orcd 
 |-  ( ( b = 1 /\ c = 5 ) -> ( -. b = 2 \/ -. c = 3 ) )
114 90 orcd 
 |-  ( ( b = 1 /\ c = 5 ) -> ( -. b = 3 \/ -. c = 2 ) )
115 113 114 jca 
 |-  ( ( b = 1 /\ c = 5 ) -> ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) )
116 101 112 115 3jca 
 |-  ( ( b = 1 /\ c = 5 ) -> ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) )
117 90 orcd 
 |-  ( ( b = 1 /\ c = 5 ) -> ( -. b = 3 \/ -. c = 4 ) )
118 65 adantr 
 |-  ( ( b = 1 /\ c = 5 ) -> b =/= 4 )
119 118 neneqd 
 |-  ( ( b = 1 /\ c = 5 ) -> -. b = 4 )
120 119 orcd 
 |-  ( ( b = 1 /\ c = 5 ) -> ( -. b = 4 \/ -. c = 3 ) )
121 117 120 jca 
 |-  ( ( b = 1 /\ c = 5 ) -> ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) )
122 119 orcd 
 |-  ( ( b = 1 /\ c = 5 ) -> ( -. b = 4 \/ -. c = 5 ) )
123 74 adantr 
 |-  ( ( b = 1 /\ c = 5 ) -> b =/= 5 )
124 123 neneqd 
 |-  ( ( b = 1 /\ c = 5 ) -> -. b = 5 )
125 124 orcd 
 |-  ( ( b = 1 /\ c = 5 ) -> ( -. b = 5 \/ -. c = 4 ) )
126 122 125 jca 
 |-  ( ( b = 1 /\ c = 5 ) -> ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) )
127 87 orcd 
 |-  ( ( b = 1 /\ c = 5 ) -> ( -. b = 0 \/ -. c = 5 ) )
128 99 olcd 
 |-  ( ( b = 1 /\ c = 5 ) -> ( -. b = 5 \/ -. c = 0 ) )
129 127 128 jca 
 |-  ( ( b = 1 /\ c = 5 ) -> ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) )
130 121 126 129 3jca 
 |-  ( ( b = 1 /\ c = 5 ) -> ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) )
131 116 130 jca 
 |-  ( ( b = 1 /\ c = 5 ) -> ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) )
132 88 91 131 jca31 
 |-  ( ( b = 1 /\ c = 5 ) -> ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) )
133 132 olcd 
 |-  ( ( b = 1 /\ c = 5 ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
134 14 85 133 3jaodan 
 |-  ( ( b = 1 /\ ( c = 1 \/ c = 3 \/ c = 5 ) ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
135 neeq1 
 |-  ( b = 3 -> ( b =/= 0 <-> 3 =/= 0 ) )
136 21 135 mpbiri 
 |-  ( b = 3 -> b =/= 0 )
137 136 adantr 
 |-  ( ( b = 3 /\ c = 1 ) -> b =/= 0 )
138 137 neneqd 
 |-  ( ( b = 3 /\ c = 1 ) -> -. b = 0 )
139 138 orcd 
 |-  ( ( b = 3 /\ c = 1 ) -> ( -. b = 0 \/ -. c = 3 ) )
140 neeq1 
 |-  ( c = 1 -> ( c =/= 0 <-> 1 =/= 0 ) )
141 15 140 mpbiri 
 |-  ( c = 1 -> c =/= 0 )
142 141 adantl 
 |-  ( ( b = 3 /\ c = 1 ) -> c =/= 0 )
143 142 neneqd 
 |-  ( ( b = 3 /\ c = 1 ) -> -. c = 0 )
144 143 olcd 
 |-  ( ( b = 3 /\ c = 1 ) -> ( -. b = 3 \/ -. c = 0 ) )
145 138 orcd 
 |-  ( ( b = 3 /\ c = 1 ) -> ( -. b = 0 \/ -. c = 1 ) )
146 143 olcd 
 |-  ( ( b = 3 /\ c = 1 ) -> ( -. b = 1 \/ -. c = 0 ) )
147 145 146 jca 
 |-  ( ( b = 3 /\ c = 1 ) -> ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) )
148 58 necon2i 
 |-  ( b = 3 -> b =/= 1 )
149 148 adantr 
 |-  ( ( b = 3 /\ c = 1 ) -> b =/= 1 )
150 149 neneqd 
 |-  ( ( b = 3 /\ c = 1 ) -> -. b = 1 )
151 150 orcd 
 |-  ( ( b = 3 /\ c = 1 ) -> ( -. b = 1 \/ -. c = 2 ) )
152 neeq1 
 |-  ( b = 3 -> ( b =/= 2 <-> 3 =/= 2 ) )
153 32 152 mpbiri 
 |-  ( b = 3 -> b =/= 2 )
154 153 adantr 
 |-  ( ( b = 3 /\ c = 1 ) -> b =/= 2 )
155 154 neneqd 
 |-  ( ( b = 3 /\ c = 1 ) -> -. b = 2 )
156 155 orcd 
 |-  ( ( b = 3 /\ c = 1 ) -> ( -. b = 2 \/ -. c = 1 ) )
157 151 156 jca 
 |-  ( ( b = 3 /\ c = 1 ) -> ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) )
158 155 orcd 
 |-  ( ( b = 3 /\ c = 1 ) -> ( -. b = 2 \/ -. c = 3 ) )
159 neeq1 
 |-  ( c = 1 -> ( c =/= 2 <-> 1 =/= 2 ) )
160 47 159 mpbiri 
 |-  ( c = 1 -> c =/= 2 )
161 160 adantl 
 |-  ( ( b = 3 /\ c = 1 ) -> c =/= 2 )
162 161 neneqd 
 |-  ( ( b = 3 /\ c = 1 ) -> -. c = 2 )
163 162 olcd 
 |-  ( ( b = 3 /\ c = 1 ) -> ( -. b = 3 \/ -. c = 2 ) )
164 158 163 jca 
 |-  ( ( b = 3 /\ c = 1 ) -> ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) )
165 147 157 164 3jca 
 |-  ( ( b = 3 /\ c = 1 ) -> ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) )
166 neeq1 
 |-  ( c = 1 -> ( c =/= 4 <-> 1 =/= 4 ) )
167 63 166 mpbiri 
 |-  ( c = 1 -> c =/= 4 )
168 167 adantl 
 |-  ( ( b = 3 /\ c = 1 ) -> c =/= 4 )
169 168 neneqd 
 |-  ( ( b = 3 /\ c = 1 ) -> -. c = 4 )
170 169 olcd 
 |-  ( ( b = 3 /\ c = 1 ) -> ( -. b = 3 \/ -. c = 4 ) )
171 42 necon2i 
 |-  ( c = 1 -> c =/= 3 )
172 171 adantl 
 |-  ( ( b = 3 /\ c = 1 ) -> c =/= 3 )
173 172 neneqd 
 |-  ( ( b = 3 /\ c = 1 ) -> -. c = 3 )
174 173 olcd 
 |-  ( ( b = 3 /\ c = 1 ) -> ( -. b = 4 \/ -. c = 3 ) )
175 170 174 jca 
 |-  ( ( b = 3 /\ c = 1 ) -> ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) )
176 neeq1 
 |-  ( c = 1 -> ( c =/= 5 <-> 1 =/= 5 ) )
177 72 176 mpbiri 
 |-  ( c = 1 -> c =/= 5 )
178 177 adantl 
 |-  ( ( b = 3 /\ c = 1 ) -> c =/= 5 )
179 178 neneqd 
 |-  ( ( b = 3 /\ c = 1 ) -> -. c = 5 )
180 179 olcd 
 |-  ( ( b = 3 /\ c = 1 ) -> ( -. b = 4 \/ -. c = 5 ) )
181 169 olcd 
 |-  ( ( b = 3 /\ c = 1 ) -> ( -. b = 5 \/ -. c = 4 ) )
182 180 181 jca 
 |-  ( ( b = 3 /\ c = 1 ) -> ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) )
183 138 orcd 
 |-  ( ( b = 3 /\ c = 1 ) -> ( -. b = 0 \/ -. c = 5 ) )
184 143 olcd 
 |-  ( ( b = 3 /\ c = 1 ) -> ( -. b = 5 \/ -. c = 0 ) )
185 183 184 jca 
 |-  ( ( b = 3 /\ c = 1 ) -> ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) )
186 175 182 185 3jca 
 |-  ( ( b = 3 /\ c = 1 ) -> ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) )
187 165 186 jca 
 |-  ( ( b = 3 /\ c = 1 ) -> ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) )
188 139 144 187 jca31 
 |-  ( ( b = 3 /\ c = 1 ) -> ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) )
189 188 olcd 
 |-  ( ( b = 3 /\ c = 1 ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
190 eqtr3 
 |-  ( ( b = 3 /\ c = 3 ) -> b = c )
191 190 orcd 
 |-  ( ( b = 3 /\ c = 3 ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
192 136 adantr 
 |-  ( ( b = 3 /\ c = 5 ) -> b =/= 0 )
193 192 neneqd 
 |-  ( ( b = 3 /\ c = 5 ) -> -. b = 0 )
194 193 orcd 
 |-  ( ( b = 3 /\ c = 5 ) -> ( -. b = 0 \/ -. c = 3 ) )
195 97 adantl 
 |-  ( ( b = 3 /\ c = 5 ) -> c =/= 0 )
196 195 neneqd 
 |-  ( ( b = 3 /\ c = 5 ) -> -. c = 0 )
197 196 olcd 
 |-  ( ( b = 3 /\ c = 5 ) -> ( -. b = 3 \/ -. c = 0 ) )
198 193 orcd 
 |-  ( ( b = 3 /\ c = 5 ) -> ( -. b = 0 \/ -. c = 1 ) )
199 196 olcd 
 |-  ( ( b = 3 /\ c = 5 ) -> ( -. b = 1 \/ -. c = 0 ) )
200 198 199 jca 
 |-  ( ( b = 3 /\ c = 5 ) -> ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) )
201 148 adantr 
 |-  ( ( b = 3 /\ c = 5 ) -> b =/= 1 )
202 201 neneqd 
 |-  ( ( b = 3 /\ c = 5 ) -> -. b = 1 )
203 202 orcd 
 |-  ( ( b = 3 /\ c = 5 ) -> ( -. b = 1 \/ -. c = 2 ) )
204 177 necon2i 
 |-  ( c = 5 -> c =/= 1 )
205 204 adantl 
 |-  ( ( b = 3 /\ c = 5 ) -> c =/= 1 )
206 205 neneqd 
 |-  ( ( b = 3 /\ c = 5 ) -> -. c = 1 )
207 206 olcd 
 |-  ( ( b = 3 /\ c = 5 ) -> ( -. b = 2 \/ -. c = 1 ) )
208 203 207 jca 
 |-  ( ( b = 3 /\ c = 5 ) -> ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) )
209 153 adantr 
 |-  ( ( b = 3 /\ c = 5 ) -> b =/= 2 )
210 209 neneqd 
 |-  ( ( b = 3 /\ c = 5 ) -> -. b = 2 )
211 210 orcd 
 |-  ( ( b = 3 /\ c = 5 ) -> ( -. b = 2 \/ -. c = 3 ) )
212 105 adantl 
 |-  ( ( b = 3 /\ c = 5 ) -> c =/= 2 )
213 212 neneqd 
 |-  ( ( b = 3 /\ c = 5 ) -> -. c = 2 )
214 213 olcd 
 |-  ( ( b = 3 /\ c = 5 ) -> ( -. b = 3 \/ -. c = 2 ) )
215 211 214 jca 
 |-  ( ( b = 3 /\ c = 5 ) -> ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) )
216 200 208 215 3jca 
 |-  ( ( b = 3 /\ c = 5 ) -> ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) )
217 4re 
 |-  4 e. RR
218 4lt5 
 |-  4 < 5
219 217 218 gtneii 
 |-  5 =/= 4
220 neeq1 
 |-  ( c = 5 -> ( c =/= 4 <-> 5 =/= 4 ) )
221 219 220 mpbiri 
 |-  ( c = 5 -> c =/= 4 )
222 221 adantl 
 |-  ( ( b = 3 /\ c = 5 ) -> c =/= 4 )
223 222 neneqd 
 |-  ( ( b = 3 /\ c = 5 ) -> -. c = 4 )
224 223 olcd 
 |-  ( ( b = 3 /\ c = 5 ) -> ( -. b = 3 \/ -. c = 4 ) )
225 3re 
 |-  3 e. RR
226 3lt4 
 |-  3 < 4
227 225 226 ltneii 
 |-  3 =/= 4
228 neeq1 
 |-  ( b = 3 -> ( b =/= 4 <-> 3 =/= 4 ) )
229 227 228 mpbiri 
 |-  ( b = 3 -> b =/= 4 )
230 229 adantr 
 |-  ( ( b = 3 /\ c = 5 ) -> b =/= 4 )
231 230 neneqd 
 |-  ( ( b = 3 /\ c = 5 ) -> -. b = 4 )
232 231 orcd 
 |-  ( ( b = 3 /\ c = 5 ) -> ( -. b = 4 \/ -. c = 3 ) )
233 224 232 jca 
 |-  ( ( b = 3 /\ c = 5 ) -> ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) )
234 231 orcd 
 |-  ( ( b = 3 /\ c = 5 ) -> ( -. b = 4 \/ -. c = 5 ) )
235 223 olcd 
 |-  ( ( b = 3 /\ c = 5 ) -> ( -. b = 5 \/ -. c = 4 ) )
236 234 235 jca 
 |-  ( ( b = 3 /\ c = 5 ) -> ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) )
237 193 orcd 
 |-  ( ( b = 3 /\ c = 5 ) -> ( -. b = 0 \/ -. c = 5 ) )
238 196 olcd 
 |-  ( ( b = 3 /\ c = 5 ) -> ( -. b = 5 \/ -. c = 0 ) )
239 237 238 jca 
 |-  ( ( b = 3 /\ c = 5 ) -> ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) )
240 233 236 239 3jca 
 |-  ( ( b = 3 /\ c = 5 ) -> ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) )
241 216 240 jca 
 |-  ( ( b = 3 /\ c = 5 ) -> ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) )
242 194 197 241 jca31 
 |-  ( ( b = 3 /\ c = 5 ) -> ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) )
243 242 olcd 
 |-  ( ( b = 3 /\ c = 5 ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
244 189 191 243 3jaodan 
 |-  ( ( b = 3 /\ ( c = 1 \/ c = 3 \/ c = 5 ) ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
245 171 adantl 
 |-  ( ( b = 5 /\ c = 1 ) -> c =/= 3 )
246 245 neneqd 
 |-  ( ( b = 5 /\ c = 1 ) -> -. c = 3 )
247 246 olcd 
 |-  ( ( b = 5 /\ c = 1 ) -> ( -. b = 0 \/ -. c = 3 ) )
248 141 adantl 
 |-  ( ( b = 5 /\ c = 1 ) -> c =/= 0 )
249 248 neneqd 
 |-  ( ( b = 5 /\ c = 1 ) -> -. c = 0 )
250 249 olcd 
 |-  ( ( b = 5 /\ c = 1 ) -> ( -. b = 3 \/ -. c = 0 ) )
251 neeq1 
 |-  ( b = 5 -> ( b =/= 0 <-> 5 =/= 0 ) )
252 95 251 mpbiri 
 |-  ( b = 5 -> b =/= 0 )
253 252 adantr 
 |-  ( ( b = 5 /\ c = 1 ) -> b =/= 0 )
254 253 neneqd 
 |-  ( ( b = 5 /\ c = 1 ) -> -. b = 0 )
255 254 orcd 
 |-  ( ( b = 5 /\ c = 1 ) -> ( -. b = 0 \/ -. c = 1 ) )
256 249 olcd 
 |-  ( ( b = 5 /\ c = 1 ) -> ( -. b = 1 \/ -. c = 0 ) )
257 255 256 jca 
 |-  ( ( b = 5 /\ c = 1 ) -> ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) )
258 74 necon2i 
 |-  ( b = 5 -> b =/= 1 )
259 258 adantr 
 |-  ( ( b = 5 /\ c = 1 ) -> b =/= 1 )
260 259 neneqd 
 |-  ( ( b = 5 /\ c = 1 ) -> -. b = 1 )
261 260 orcd 
 |-  ( ( b = 5 /\ c = 1 ) -> ( -. b = 1 \/ -. c = 2 ) )
262 neeq1 
 |-  ( b = 5 -> ( b =/= 2 <-> 5 =/= 2 ) )
263 103 262 mpbiri 
 |-  ( b = 5 -> b =/= 2 )
264 263 adantr 
 |-  ( ( b = 5 /\ c = 1 ) -> b =/= 2 )
265 264 neneqd 
 |-  ( ( b = 5 /\ c = 1 ) -> -. b = 2 )
266 265 orcd 
 |-  ( ( b = 5 /\ c = 1 ) -> ( -. b = 2 \/ -. c = 1 ) )
267 261 266 jca 
 |-  ( ( b = 5 /\ c = 1 ) -> ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) )
268 246 olcd 
 |-  ( ( b = 5 /\ c = 1 ) -> ( -. b = 2 \/ -. c = 3 ) )
269 160 adantl 
 |-  ( ( b = 5 /\ c = 1 ) -> c =/= 2 )
270 269 neneqd 
 |-  ( ( b = 5 /\ c = 1 ) -> -. c = 2 )
271 270 olcd 
 |-  ( ( b = 5 /\ c = 1 ) -> ( -. b = 3 \/ -. c = 2 ) )
272 268 271 jca 
 |-  ( ( b = 5 /\ c = 1 ) -> ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) )
273 257 267 272 3jca 
 |-  ( ( b = 5 /\ c = 1 ) -> ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) )
274 3lt5 
 |-  3 < 5
275 225 274 gtneii 
 |-  5 =/= 3
276 neeq1 
 |-  ( b = 5 -> ( b =/= 3 <-> 5 =/= 3 ) )
277 275 276 mpbiri 
 |-  ( b = 5 -> b =/= 3 )
278 277 adantr 
 |-  ( ( b = 5 /\ c = 1 ) -> b =/= 3 )
279 278 neneqd 
 |-  ( ( b = 5 /\ c = 1 ) -> -. b = 3 )
280 279 orcd 
 |-  ( ( b = 5 /\ c = 1 ) -> ( -. b = 3 \/ -. c = 4 ) )
281 246 olcd 
 |-  ( ( b = 5 /\ c = 1 ) -> ( -. b = 4 \/ -. c = 3 ) )
282 280 281 jca 
 |-  ( ( b = 5 /\ c = 1 ) -> ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) )
283 177 adantl 
 |-  ( ( b = 5 /\ c = 1 ) -> c =/= 5 )
284 283 neneqd 
 |-  ( ( b = 5 /\ c = 1 ) -> -. c = 5 )
285 284 olcd 
 |-  ( ( b = 5 /\ c = 1 ) -> ( -. b = 4 \/ -. c = 5 ) )
286 167 adantl 
 |-  ( ( b = 5 /\ c = 1 ) -> c =/= 4 )
287 286 neneqd 
 |-  ( ( b = 5 /\ c = 1 ) -> -. c = 4 )
288 287 olcd 
 |-  ( ( b = 5 /\ c = 1 ) -> ( -. b = 5 \/ -. c = 4 ) )
289 285 288 jca 
 |-  ( ( b = 5 /\ c = 1 ) -> ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) )
290 254 orcd 
 |-  ( ( b = 5 /\ c = 1 ) -> ( -. b = 0 \/ -. c = 5 ) )
291 249 olcd 
 |-  ( ( b = 5 /\ c = 1 ) -> ( -. b = 5 \/ -. c = 0 ) )
292 290 291 jca 
 |-  ( ( b = 5 /\ c = 1 ) -> ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) )
293 282 289 292 3jca 
 |-  ( ( b = 5 /\ c = 1 ) -> ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) )
294 273 293 jca 
 |-  ( ( b = 5 /\ c = 1 ) -> ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) )
295 247 250 294 jca31 
 |-  ( ( b = 5 /\ c = 1 ) -> ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) )
296 295 olcd 
 |-  ( ( b = 5 /\ c = 1 ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
297 252 adantr 
 |-  ( ( b = 5 /\ c = 3 ) -> b =/= 0 )
298 297 neneqd 
 |-  ( ( b = 5 /\ c = 3 ) -> -. b = 0 )
299 298 orcd 
 |-  ( ( b = 5 /\ c = 3 ) -> ( -. b = 0 \/ -. c = 3 ) )
300 23 adantl 
 |-  ( ( b = 5 /\ c = 3 ) -> c =/= 0 )
301 300 neneqd 
 |-  ( ( b = 5 /\ c = 3 ) -> -. c = 0 )
302 301 olcd 
 |-  ( ( b = 5 /\ c = 3 ) -> ( -. b = 3 \/ -. c = 0 ) )
303 298 orcd 
 |-  ( ( b = 5 /\ c = 3 ) -> ( -. b = 0 \/ -. c = 1 ) )
304 301 olcd 
 |-  ( ( b = 5 /\ c = 3 ) -> ( -. b = 1 \/ -. c = 0 ) )
305 303 304 jca 
 |-  ( ( b = 5 /\ c = 3 ) -> ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) )
306 258 adantr 
 |-  ( ( b = 5 /\ c = 3 ) -> b =/= 1 )
307 306 neneqd 
 |-  ( ( b = 5 /\ c = 3 ) -> -. b = 1 )
308 307 orcd 
 |-  ( ( b = 5 /\ c = 3 ) -> ( -. b = 1 \/ -. c = 2 ) )
309 42 adantl 
 |-  ( ( b = 5 /\ c = 3 ) -> c =/= 1 )
310 309 neneqd 
 |-  ( ( b = 5 /\ c = 3 ) -> -. c = 1 )
311 310 olcd 
 |-  ( ( b = 5 /\ c = 3 ) -> ( -. b = 2 \/ -. c = 1 ) )
312 308 311 jca 
 |-  ( ( b = 5 /\ c = 3 ) -> ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) )
313 263 adantr 
 |-  ( ( b = 5 /\ c = 3 ) -> b =/= 2 )
314 313 neneqd 
 |-  ( ( b = 5 /\ c = 3 ) -> -. b = 2 )
315 314 orcd 
 |-  ( ( b = 5 /\ c = 3 ) -> ( -. b = 2 \/ -. c = 3 ) )
316 277 adantr 
 |-  ( ( b = 5 /\ c = 3 ) -> b =/= 3 )
317 316 neneqd 
 |-  ( ( b = 5 /\ c = 3 ) -> -. b = 3 )
318 317 orcd 
 |-  ( ( b = 5 /\ c = 3 ) -> ( -. b = 3 \/ -. c = 2 ) )
319 315 318 jca 
 |-  ( ( b = 5 /\ c = 3 ) -> ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) )
320 305 312 319 3jca 
 |-  ( ( b = 5 /\ c = 3 ) -> ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) )
321 317 orcd 
 |-  ( ( b = 5 /\ c = 3 ) -> ( -. b = 3 \/ -. c = 4 ) )
322 neeq1 
 |-  ( b = 5 -> ( b =/= 4 <-> 5 =/= 4 ) )
323 219 322 mpbiri 
 |-  ( b = 5 -> b =/= 4 )
324 323 adantr 
 |-  ( ( b = 5 /\ c = 3 ) -> b =/= 4 )
325 324 neneqd 
 |-  ( ( b = 5 /\ c = 3 ) -> -. b = 4 )
326 325 orcd 
 |-  ( ( b = 5 /\ c = 3 ) -> ( -. b = 4 \/ -. c = 3 ) )
327 321 326 jca 
 |-  ( ( b = 5 /\ c = 3 ) -> ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) )
328 325 orcd 
 |-  ( ( b = 5 /\ c = 3 ) -> ( -. b = 4 \/ -. c = 5 ) )
329 neeq1 
 |-  ( c = 3 -> ( c =/= 4 <-> 3 =/= 4 ) )
330 227 329 mpbiri 
 |-  ( c = 3 -> c =/= 4 )
331 330 adantl 
 |-  ( ( b = 5 /\ c = 3 ) -> c =/= 4 )
332 331 neneqd 
 |-  ( ( b = 5 /\ c = 3 ) -> -. c = 4 )
333 332 olcd 
 |-  ( ( b = 5 /\ c = 3 ) -> ( -. b = 5 \/ -. c = 4 ) )
334 328 333 jca 
 |-  ( ( b = 5 /\ c = 3 ) -> ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) )
335 298 orcd 
 |-  ( ( b = 5 /\ c = 3 ) -> ( -. b = 0 \/ -. c = 5 ) )
336 301 olcd 
 |-  ( ( b = 5 /\ c = 3 ) -> ( -. b = 5 \/ -. c = 0 ) )
337 335 336 jca 
 |-  ( ( b = 5 /\ c = 3 ) -> ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) )
338 327 334 337 3jca 
 |-  ( ( b = 5 /\ c = 3 ) -> ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) )
339 320 338 jca 
 |-  ( ( b = 5 /\ c = 3 ) -> ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) )
340 299 302 339 jca31 
 |-  ( ( b = 5 /\ c = 3 ) -> ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) )
341 340 olcd 
 |-  ( ( b = 5 /\ c = 3 ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
342 eqtr3 
 |-  ( ( b = 5 /\ c = 5 ) -> b = c )
343 342 orcd 
 |-  ( ( b = 5 /\ c = 5 ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
344 296 341 343 3jaodan 
 |-  ( ( b = 5 /\ ( c = 1 \/ c = 3 \/ c = 5 ) ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
345 134 244 344 3jaoian 
 |-  ( ( ( b = 1 \/ b = 3 \/ b = 5 ) /\ ( c = 1 \/ c = 3 \/ c = 5 ) ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
346 8 12 345 syl2anb 
 |-  ( ( b e. ( G NeighbVtx 0 ) /\ c e. ( G NeighbVtx 0 ) ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
347 346 rgen2 
 |-  A. b e. ( G NeighbVtx 0 ) A. c e. ( G NeighbVtx 0 ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) )
348 1 2 3 usgrexmpl2nb1 
 |-  ( G NeighbVtx 1 ) = { 0 , 2 }
349 348 eleq2i 
 |-  ( b e. ( G NeighbVtx 1 ) <-> b e. { 0 , 2 } )
350 6 elpr 
 |-  ( b e. { 0 , 2 } <-> ( b = 0 \/ b = 2 ) )
351 349 350 bitri 
 |-  ( b e. ( G NeighbVtx 1 ) <-> ( b = 0 \/ b = 2 ) )
352 348 eleq2i 
 |-  ( c e. ( G NeighbVtx 1 ) <-> c e. { 0 , 2 } )
353 10 elpr 
 |-  ( c e. { 0 , 2 } <-> ( c = 0 \/ c = 2 ) )
354 352 353 bitri 
 |-  ( c e. ( G NeighbVtx 1 ) <-> ( c = 0 \/ c = 2 ) )
355 eqtr3 
 |-  ( ( b = 0 /\ c = 0 ) -> b = c )
356 355 orcd 
 |-  ( ( b = 0 /\ c = 0 ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
357 2ne0 
 |-  2 =/= 0
358 neeq1 
 |-  ( b = 2 -> ( b =/= 0 <-> 2 =/= 0 ) )
359 357 358 mpbiri 
 |-  ( b = 2 -> b =/= 0 )
360 359 adantr 
 |-  ( ( b = 2 /\ c = 0 ) -> b =/= 0 )
361 360 neneqd 
 |-  ( ( b = 2 /\ c = 0 ) -> -. b = 0 )
362 361 orcd 
 |-  ( ( b = 2 /\ c = 0 ) -> ( -. b = 0 \/ -. c = 3 ) )
363 153 necon2i 
 |-  ( b = 2 -> b =/= 3 )
364 363 adantr 
 |-  ( ( b = 2 /\ c = 0 ) -> b =/= 3 )
365 364 neneqd 
 |-  ( ( b = 2 /\ c = 0 ) -> -. b = 3 )
366 365 orcd 
 |-  ( ( b = 2 /\ c = 0 ) -> ( -. b = 3 \/ -. c = 0 ) )
367 361 orcd 
 |-  ( ( b = 2 /\ c = 0 ) -> ( -. b = 0 \/ -. c = 1 ) )
368 49 necon2i 
 |-  ( b = 2 -> b =/= 1 )
369 368 adantr 
 |-  ( ( b = 2 /\ c = 0 ) -> b =/= 1 )
370 369 neneqd 
 |-  ( ( b = 2 /\ c = 0 ) -> -. b = 1 )
371 370 orcd 
 |-  ( ( b = 2 /\ c = 0 ) -> ( -. b = 1 \/ -. c = 0 ) )
372 367 371 jca 
 |-  ( ( b = 2 /\ c = 0 ) -> ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) )
373 370 orcd 
 |-  ( ( b = 2 /\ c = 0 ) -> ( -. b = 1 \/ -. c = 2 ) )
374 141 necon2i 
 |-  ( c = 0 -> c =/= 1 )
375 374 adantl 
 |-  ( ( b = 2 /\ c = 0 ) -> c =/= 1 )
376 375 neneqd 
 |-  ( ( b = 2 /\ c = 0 ) -> -. c = 1 )
377 376 olcd 
 |-  ( ( b = 2 /\ c = 0 ) -> ( -. b = 2 \/ -. c = 1 ) )
378 373 377 jca 
 |-  ( ( b = 2 /\ c = 0 ) -> ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) )
379 23 necon2i 
 |-  ( c = 0 -> c =/= 3 )
380 379 adantl 
 |-  ( ( b = 2 /\ c = 0 ) -> c =/= 3 )
381 380 neneqd 
 |-  ( ( b = 2 /\ c = 0 ) -> -. c = 3 )
382 381 olcd 
 |-  ( ( b = 2 /\ c = 0 ) -> ( -. b = 2 \/ -. c = 3 ) )
383 365 orcd 
 |-  ( ( b = 2 /\ c = 0 ) -> ( -. b = 3 \/ -. c = 2 ) )
384 382 383 jca 
 |-  ( ( b = 2 /\ c = 0 ) -> ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) )
385 372 378 384 3jca 
 |-  ( ( b = 2 /\ c = 0 ) -> ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) )
386 365 orcd 
 |-  ( ( b = 2 /\ c = 0 ) -> ( -. b = 3 \/ -. c = 4 ) )
387 381 olcd 
 |-  ( ( b = 2 /\ c = 0 ) -> ( -. b = 4 \/ -. c = 3 ) )
388 386 387 jca 
 |-  ( ( b = 2 /\ c = 0 ) -> ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) )
389 97 necon2i 
 |-  ( c = 0 -> c =/= 5 )
390 389 adantl 
 |-  ( ( b = 2 /\ c = 0 ) -> c =/= 5 )
391 390 neneqd 
 |-  ( ( b = 2 /\ c = 0 ) -> -. c = 5 )
392 391 olcd 
 |-  ( ( b = 2 /\ c = 0 ) -> ( -. b = 4 \/ -. c = 5 ) )
393 4pos 
 |-  0 < 4
394 93 393 ltneii 
 |-  0 =/= 4
395 neeq1 
 |-  ( c = 0 -> ( c =/= 4 <-> 0 =/= 4 ) )
396 394 395 mpbiri 
 |-  ( c = 0 -> c =/= 4 )
397 396 adantl 
 |-  ( ( b = 2 /\ c = 0 ) -> c =/= 4 )
398 397 neneqd 
 |-  ( ( b = 2 /\ c = 0 ) -> -. c = 4 )
399 398 olcd 
 |-  ( ( b = 2 /\ c = 0 ) -> ( -. b = 5 \/ -. c = 4 ) )
400 392 399 jca 
 |-  ( ( b = 2 /\ c = 0 ) -> ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) )
401 361 orcd 
 |-  ( ( b = 2 /\ c = 0 ) -> ( -. b = 0 \/ -. c = 5 ) )
402 263 necon2i 
 |-  ( b = 2 -> b =/= 5 )
403 402 adantr 
 |-  ( ( b = 2 /\ c = 0 ) -> b =/= 5 )
404 403 neneqd 
 |-  ( ( b = 2 /\ c = 0 ) -> -. b = 5 )
405 404 orcd 
 |-  ( ( b = 2 /\ c = 0 ) -> ( -. b = 5 \/ -. c = 0 ) )
406 401 405 jca 
 |-  ( ( b = 2 /\ c = 0 ) -> ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) )
407 388 400 406 3jca 
 |-  ( ( b = 2 /\ c = 0 ) -> ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) )
408 385 407 jca 
 |-  ( ( b = 2 /\ c = 0 ) -> ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) )
409 362 366 408 jca31 
 |-  ( ( b = 2 /\ c = 0 ) -> ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) )
410 409 olcd 
 |-  ( ( b = 2 /\ c = 0 ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
411 34 necon2i 
 |-  ( c = 2 -> c =/= 3 )
412 411 adantl 
 |-  ( ( b = 0 /\ c = 2 ) -> c =/= 3 )
413 412 neneqd 
 |-  ( ( b = 0 /\ c = 2 ) -> -. c = 3 )
414 413 olcd 
 |-  ( ( b = 0 /\ c = 2 ) -> ( -. b = 0 \/ -. c = 3 ) )
415 neeq1 
 |-  ( c = 2 -> ( c =/= 0 <-> 2 =/= 0 ) )
416 357 415 mpbiri 
 |-  ( c = 2 -> c =/= 0 )
417 416 adantl 
 |-  ( ( b = 0 /\ c = 2 ) -> c =/= 0 )
418 417 neneqd 
 |-  ( ( b = 0 /\ c = 2 ) -> -. c = 0 )
419 418 olcd 
 |-  ( ( b = 0 /\ c = 2 ) -> ( -. b = 3 \/ -. c = 0 ) )
420 160 necon2i 
 |-  ( c = 2 -> c =/= 1 )
421 420 adantl 
 |-  ( ( b = 0 /\ c = 2 ) -> c =/= 1 )
422 421 neneqd 
 |-  ( ( b = 0 /\ c = 2 ) -> -. c = 1 )
423 422 olcd 
 |-  ( ( b = 0 /\ c = 2 ) -> ( -. b = 0 \/ -. c = 1 ) )
424 418 olcd 
 |-  ( ( b = 0 /\ c = 2 ) -> ( -. b = 1 \/ -. c = 0 ) )
425 423 424 jca 
 |-  ( ( b = 0 /\ c = 2 ) -> ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) )
426 17 necon2i 
 |-  ( b = 0 -> b =/= 1 )
427 426 adantr 
 |-  ( ( b = 0 /\ c = 2 ) -> b =/= 1 )
428 427 neneqd 
 |-  ( ( b = 0 /\ c = 2 ) -> -. b = 1 )
429 428 orcd 
 |-  ( ( b = 0 /\ c = 2 ) -> ( -. b = 1 \/ -. c = 2 ) )
430 359 necon2i 
 |-  ( b = 0 -> b =/= 2 )
431 430 adantr 
 |-  ( ( b = 0 /\ c = 2 ) -> b =/= 2 )
432 431 neneqd 
 |-  ( ( b = 0 /\ c = 2 ) -> -. b = 2 )
433 432 orcd 
 |-  ( ( b = 0 /\ c = 2 ) -> ( -. b = 2 \/ -. c = 1 ) )
434 429 433 jca 
 |-  ( ( b = 0 /\ c = 2 ) -> ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) )
435 413 olcd 
 |-  ( ( b = 0 /\ c = 2 ) -> ( -. b = 2 \/ -. c = 3 ) )
436 136 necon2i 
 |-  ( b = 0 -> b =/= 3 )
437 436 adantr 
 |-  ( ( b = 0 /\ c = 2 ) -> b =/= 3 )
438 437 neneqd 
 |-  ( ( b = 0 /\ c = 2 ) -> -. b = 3 )
439 438 orcd 
 |-  ( ( b = 0 /\ c = 2 ) -> ( -. b = 3 \/ -. c = 2 ) )
440 435 439 jca 
 |-  ( ( b = 0 /\ c = 2 ) -> ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) )
441 425 434 440 3jca 
 |-  ( ( b = 0 /\ c = 2 ) -> ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) )
442 438 orcd 
 |-  ( ( b = 0 /\ c = 2 ) -> ( -. b = 3 \/ -. c = 4 ) )
443 413 olcd 
 |-  ( ( b = 0 /\ c = 2 ) -> ( -. b = 4 \/ -. c = 3 ) )
444 442 443 jca 
 |-  ( ( b = 0 /\ c = 2 ) -> ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) )
445 neeq1 
 |-  ( b = 0 -> ( b =/= 4 <-> 0 =/= 4 ) )
446 394 445 mpbiri 
 |-  ( b = 0 -> b =/= 4 )
447 446 adantr 
 |-  ( ( b = 0 /\ c = 2 ) -> b =/= 4 )
448 447 neneqd 
 |-  ( ( b = 0 /\ c = 2 ) -> -. b = 4 )
449 448 orcd 
 |-  ( ( b = 0 /\ c = 2 ) -> ( -. b = 4 \/ -. c = 5 ) )
450 252 necon2i 
 |-  ( b = 0 -> b =/= 5 )
451 450 adantr 
 |-  ( ( b = 0 /\ c = 2 ) -> b =/= 5 )
452 451 neneqd 
 |-  ( ( b = 0 /\ c = 2 ) -> -. b = 5 )
453 452 orcd 
 |-  ( ( b = 0 /\ c = 2 ) -> ( -. b = 5 \/ -. c = 4 ) )
454 449 453 jca 
 |-  ( ( b = 0 /\ c = 2 ) -> ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) )
455 105 necon2i 
 |-  ( c = 2 -> c =/= 5 )
456 455 adantl 
 |-  ( ( b = 0 /\ c = 2 ) -> c =/= 5 )
457 456 neneqd 
 |-  ( ( b = 0 /\ c = 2 ) -> -. c = 5 )
458 457 olcd 
 |-  ( ( b = 0 /\ c = 2 ) -> ( -. b = 0 \/ -. c = 5 ) )
459 418 olcd 
 |-  ( ( b = 0 /\ c = 2 ) -> ( -. b = 5 \/ -. c = 0 ) )
460 458 459 jca 
 |-  ( ( b = 0 /\ c = 2 ) -> ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) )
461 444 454 460 3jca 
 |-  ( ( b = 0 /\ c = 2 ) -> ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) )
462 441 461 jca 
 |-  ( ( b = 0 /\ c = 2 ) -> ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) )
463 414 419 462 jca31 
 |-  ( ( b = 0 /\ c = 2 ) -> ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) )
464 463 olcd 
 |-  ( ( b = 0 /\ c = 2 ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
465 359 adantr 
 |-  ( ( b = 2 /\ c = 2 ) -> b =/= 0 )
466 465 neneqd 
 |-  ( ( b = 2 /\ c = 2 ) -> -. b = 0 )
467 466 orcd 
 |-  ( ( b = 2 /\ c = 2 ) -> ( -. b = 0 \/ -. c = 3 ) )
468 416 adantl 
 |-  ( ( b = 2 /\ c = 2 ) -> c =/= 0 )
469 468 neneqd 
 |-  ( ( b = 2 /\ c = 2 ) -> -. c = 0 )
470 469 olcd 
 |-  ( ( b = 2 /\ c = 2 ) -> ( -. b = 3 \/ -. c = 0 ) )
471 466 orcd 
 |-  ( ( b = 2 /\ c = 2 ) -> ( -. b = 0 \/ -. c = 1 ) )
472 469 olcd 
 |-  ( ( b = 2 /\ c = 2 ) -> ( -. b = 1 \/ -. c = 0 ) )
473 471 472 jca 
 |-  ( ( b = 2 /\ c = 2 ) -> ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) )
474 368 adantr 
 |-  ( ( b = 2 /\ c = 2 ) -> b =/= 1 )
475 474 neneqd 
 |-  ( ( b = 2 /\ c = 2 ) -> -. b = 1 )
476 475 orcd 
 |-  ( ( b = 2 /\ c = 2 ) -> ( -. b = 1 \/ -. c = 2 ) )
477 420 adantl 
 |-  ( ( b = 2 /\ c = 2 ) -> c =/= 1 )
478 477 neneqd 
 |-  ( ( b = 2 /\ c = 2 ) -> -. c = 1 )
479 478 olcd 
 |-  ( ( b = 2 /\ c = 2 ) -> ( -. b = 2 \/ -. c = 1 ) )
480 476 479 jca 
 |-  ( ( b = 2 /\ c = 2 ) -> ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) )
481 411 adantl 
 |-  ( ( b = 2 /\ c = 2 ) -> c =/= 3 )
482 481 neneqd 
 |-  ( ( b = 2 /\ c = 2 ) -> -. c = 3 )
483 482 olcd 
 |-  ( ( b = 2 /\ c = 2 ) -> ( -. b = 2 \/ -. c = 3 ) )
484 363 adantr 
 |-  ( ( b = 2 /\ c = 2 ) -> b =/= 3 )
485 484 neneqd 
 |-  ( ( b = 2 /\ c = 2 ) -> -. b = 3 )
486 485 orcd 
 |-  ( ( b = 2 /\ c = 2 ) -> ( -. b = 3 \/ -. c = 2 ) )
487 483 486 jca 
 |-  ( ( b = 2 /\ c = 2 ) -> ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) )
488 473 480 487 3jca 
 |-  ( ( b = 2 /\ c = 2 ) -> ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) )
489 485 orcd 
 |-  ( ( b = 2 /\ c = 2 ) -> ( -. b = 3 \/ -. c = 4 ) )
490 2lt4 
 |-  2 < 4
491 30 490 ltneii 
 |-  2 =/= 4
492 neeq1 
 |-  ( b = 2 -> ( b =/= 4 <-> 2 =/= 4 ) )
493 491 492 mpbiri 
 |-  ( b = 2 -> b =/= 4 )
494 493 adantr 
 |-  ( ( b = 2 /\ c = 2 ) -> b =/= 4 )
495 494 neneqd 
 |-  ( ( b = 2 /\ c = 2 ) -> -. b = 4 )
496 495 orcd 
 |-  ( ( b = 2 /\ c = 2 ) -> ( -. b = 4 \/ -. c = 3 ) )
497 489 496 jca 
 |-  ( ( b = 2 /\ c = 2 ) -> ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) )
498 495 orcd 
 |-  ( ( b = 2 /\ c = 2 ) -> ( -. b = 4 \/ -. c = 5 ) )
499 402 adantr 
 |-  ( ( b = 2 /\ c = 2 ) -> b =/= 5 )
500 499 neneqd 
 |-  ( ( b = 2 /\ c = 2 ) -> -. b = 5 )
501 500 orcd 
 |-  ( ( b = 2 /\ c = 2 ) -> ( -. b = 5 \/ -. c = 4 ) )
502 498 501 jca 
 |-  ( ( b = 2 /\ c = 2 ) -> ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) )
503 466 orcd 
 |-  ( ( b = 2 /\ c = 2 ) -> ( -. b = 0 \/ -. c = 5 ) )
504 469 olcd 
 |-  ( ( b = 2 /\ c = 2 ) -> ( -. b = 5 \/ -. c = 0 ) )
505 503 504 jca 
 |-  ( ( b = 2 /\ c = 2 ) -> ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) )
506 497 502 505 3jca 
 |-  ( ( b = 2 /\ c = 2 ) -> ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) )
507 488 506 jca 
 |-  ( ( b = 2 /\ c = 2 ) -> ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) )
508 467 470 507 jca31 
 |-  ( ( b = 2 /\ c = 2 ) -> ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) )
509 508 olcd 
 |-  ( ( b = 2 /\ c = 2 ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
510 356 410 464 509 ccase 
 |-  ( ( ( b = 0 \/ b = 2 ) /\ ( c = 0 \/ c = 2 ) ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
511 351 354 510 syl2anb 
 |-  ( ( b e. ( G NeighbVtx 1 ) /\ c e. ( G NeighbVtx 1 ) ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
512 511 rgen2 
 |-  A. b e. ( G NeighbVtx 1 ) A. c e. ( G NeighbVtx 1 ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) )
513 1 2 3 usgrexmpl2nb2 
 |-  ( G NeighbVtx 2 ) = { 1 , 3 }
514 513 eleq2i 
 |-  ( b e. ( G NeighbVtx 2 ) <-> b e. { 1 , 3 } )
515 6 elpr 
 |-  ( b e. { 1 , 3 } <-> ( b = 1 \/ b = 3 ) )
516 514 515 bitri 
 |-  ( b e. ( G NeighbVtx 2 ) <-> ( b = 1 \/ b = 3 ) )
517 513 eleq2i 
 |-  ( c e. ( G NeighbVtx 2 ) <-> c e. { 1 , 3 } )
518 10 elpr 
 |-  ( c e. { 1 , 3 } <-> ( c = 1 \/ c = 3 ) )
519 517 518 bitri 
 |-  ( c e. ( G NeighbVtx 2 ) <-> ( c = 1 \/ c = 3 ) )
520 14 189 85 191 ccase 
 |-  ( ( ( b = 1 \/ b = 3 ) /\ ( c = 1 \/ c = 3 ) ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
521 516 519 520 syl2anb 
 |-  ( ( b e. ( G NeighbVtx 2 ) /\ c e. ( G NeighbVtx 2 ) ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
522 521 rgen2 
 |-  A. b e. ( G NeighbVtx 2 ) A. c e. ( G NeighbVtx 2 ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) )
523 c0ex 
 |-  0 e. _V
524 1ex 
 |-  1 e. _V
525 2ex 
 |-  2 e. _V
526 oveq2 
 |-  ( a = 0 -> ( G NeighbVtx a ) = ( G NeighbVtx 0 ) )
527 526 raleqdv 
 |-  ( a = 0 -> ( A. c e. ( G NeighbVtx a ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) <-> A. c e. ( G NeighbVtx 0 ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) ) )
528 526 527 raleqbidv 
 |-  ( a = 0 -> ( A. b e. ( G NeighbVtx a ) A. c e. ( G NeighbVtx a ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) <-> A. b e. ( G NeighbVtx 0 ) A. c e. ( G NeighbVtx 0 ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) ) )
529 oveq2 
 |-  ( a = 1 -> ( G NeighbVtx a ) = ( G NeighbVtx 1 ) )
530 529 raleqdv 
 |-  ( a = 1 -> ( A. c e. ( G NeighbVtx a ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) <-> A. c e. ( G NeighbVtx 1 ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) ) )
531 529 530 raleqbidv 
 |-  ( a = 1 -> ( A. b e. ( G NeighbVtx a ) A. c e. ( G NeighbVtx a ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) <-> A. b e. ( G NeighbVtx 1 ) A. c e. ( G NeighbVtx 1 ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) ) )
532 oveq2 
 |-  ( a = 2 -> ( G NeighbVtx a ) = ( G NeighbVtx 2 ) )
533 532 raleqdv 
 |-  ( a = 2 -> ( A. c e. ( G NeighbVtx a ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) <-> A. c e. ( G NeighbVtx 2 ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) ) )
534 532 533 raleqbidv 
 |-  ( a = 2 -> ( A. b e. ( G NeighbVtx a ) A. c e. ( G NeighbVtx a ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) <-> A. b e. ( G NeighbVtx 2 ) A. c e. ( G NeighbVtx 2 ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) ) )
535 523 524 525 528 531 534 raltp 
 |-  ( A. a e. { 0 , 1 , 2 } A. b e. ( G NeighbVtx a ) A. c e. ( G NeighbVtx a ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) <-> ( A. b e. ( G NeighbVtx 0 ) A. c e. ( G NeighbVtx 0 ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) /\ A. b e. ( G NeighbVtx 1 ) A. c e. ( G NeighbVtx 1 ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) /\ A. b e. ( G NeighbVtx 2 ) A. c e. ( G NeighbVtx 2 ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) ) )
536 347 512 522 535 mpbir3an 
 |-  A. a e. { 0 , 1 , 2 } A. b e. ( G NeighbVtx a ) A. c e. ( G NeighbVtx a ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) )
537 1 2 3 usgrexmpl2nb3 
 |-  ( G NeighbVtx 3 ) = { 0 , 2 , 4 }
538 537 eleq2i 
 |-  ( b e. ( G NeighbVtx 3 ) <-> b e. { 0 , 2 , 4 } )
539 6 eltp 
 |-  ( b e. { 0 , 2 , 4 } <-> ( b = 0 \/ b = 2 \/ b = 4 ) )
540 538 539 bitri 
 |-  ( b e. ( G NeighbVtx 3 ) <-> ( b = 0 \/ b = 2 \/ b = 4 ) )
541 537 eleq2i 
 |-  ( c e. ( G NeighbVtx 3 ) <-> c e. { 0 , 2 , 4 } )
542 10 eltp 
 |-  ( c e. { 0 , 2 , 4 } <-> ( c = 0 \/ c = 2 \/ c = 4 ) )
543 541 542 bitri 
 |-  ( c e. ( G NeighbVtx 3 ) <-> ( c = 0 \/ c = 2 \/ c = 4 ) )
544 330 necon2i 
 |-  ( c = 4 -> c =/= 3 )
545 544 adantl 
 |-  ( ( b = 0 /\ c = 4 ) -> c =/= 3 )
546 545 neneqd 
 |-  ( ( b = 0 /\ c = 4 ) -> -. c = 3 )
547 546 olcd 
 |-  ( ( b = 0 /\ c = 4 ) -> ( -. b = 0 \/ -. c = 3 ) )
548 436 adantr 
 |-  ( ( b = 0 /\ c = 4 ) -> b =/= 3 )
549 548 neneqd 
 |-  ( ( b = 0 /\ c = 4 ) -> -. b = 3 )
550 549 orcd 
 |-  ( ( b = 0 /\ c = 4 ) -> ( -. b = 3 \/ -. c = 0 ) )
551 167 necon2i 
 |-  ( c = 4 -> c =/= 1 )
552 551 adantl 
 |-  ( ( b = 0 /\ c = 4 ) -> c =/= 1 )
553 552 neneqd 
 |-  ( ( b = 0 /\ c = 4 ) -> -. c = 1 )
554 553 olcd 
 |-  ( ( b = 0 /\ c = 4 ) -> ( -. b = 0 \/ -. c = 1 ) )
555 426 adantr 
 |-  ( ( b = 0 /\ c = 4 ) -> b =/= 1 )
556 555 neneqd 
 |-  ( ( b = 0 /\ c = 4 ) -> -. b = 1 )
557 556 orcd 
 |-  ( ( b = 0 /\ c = 4 ) -> ( -. b = 1 \/ -. c = 0 ) )
558 554 557 jca 
 |-  ( ( b = 0 /\ c = 4 ) -> ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) )
559 556 orcd 
 |-  ( ( b = 0 /\ c = 4 ) -> ( -. b = 1 \/ -. c = 2 ) )
560 430 adantr 
 |-  ( ( b = 0 /\ c = 4 ) -> b =/= 2 )
561 560 neneqd 
 |-  ( ( b = 0 /\ c = 4 ) -> -. b = 2 )
562 561 orcd 
 |-  ( ( b = 0 /\ c = 4 ) -> ( -. b = 2 \/ -. c = 1 ) )
563 559 562 jca 
 |-  ( ( b = 0 /\ c = 4 ) -> ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) )
564 546 olcd 
 |-  ( ( b = 0 /\ c = 4 ) -> ( -. b = 2 \/ -. c = 3 ) )
565 549 orcd 
 |-  ( ( b = 0 /\ c = 4 ) -> ( -. b = 3 \/ -. c = 2 ) )
566 564 565 jca 
 |-  ( ( b = 0 /\ c = 4 ) -> ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) )
567 558 563 566 3jca 
 |-  ( ( b = 0 /\ c = 4 ) -> ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) )
568 549 orcd 
 |-  ( ( b = 0 /\ c = 4 ) -> ( -. b = 3 \/ -. c = 4 ) )
569 546 olcd 
 |-  ( ( b = 0 /\ c = 4 ) -> ( -. b = 4 \/ -. c = 3 ) )
570 568 569 jca 
 |-  ( ( b = 0 /\ c = 4 ) -> ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) )
571 446 adantr 
 |-  ( ( b = 0 /\ c = 4 ) -> b =/= 4 )
572 571 neneqd 
 |-  ( ( b = 0 /\ c = 4 ) -> -. b = 4 )
573 572 orcd 
 |-  ( ( b = 0 /\ c = 4 ) -> ( -. b = 4 \/ -. c = 5 ) )
574 450 adantr 
 |-  ( ( b = 0 /\ c = 4 ) -> b =/= 5 )
575 574 neneqd 
 |-  ( ( b = 0 /\ c = 4 ) -> -. b = 5 )
576 575 orcd 
 |-  ( ( b = 0 /\ c = 4 ) -> ( -. b = 5 \/ -. c = 4 ) )
577 573 576 jca 
 |-  ( ( b = 0 /\ c = 4 ) -> ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) )
578 221 necon2i 
 |-  ( c = 4 -> c =/= 5 )
579 578 adantl 
 |-  ( ( b = 0 /\ c = 4 ) -> c =/= 5 )
580 579 neneqd 
 |-  ( ( b = 0 /\ c = 4 ) -> -. c = 5 )
581 580 olcd 
 |-  ( ( b = 0 /\ c = 4 ) -> ( -. b = 0 \/ -. c = 5 ) )
582 396 necon2i 
 |-  ( c = 4 -> c =/= 0 )
583 582 adantl 
 |-  ( ( b = 0 /\ c = 4 ) -> c =/= 0 )
584 583 neneqd 
 |-  ( ( b = 0 /\ c = 4 ) -> -. c = 0 )
585 584 olcd 
 |-  ( ( b = 0 /\ c = 4 ) -> ( -. b = 5 \/ -. c = 0 ) )
586 581 585 jca 
 |-  ( ( b = 0 /\ c = 4 ) -> ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) )
587 570 577 586 3jca 
 |-  ( ( b = 0 /\ c = 4 ) -> ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) )
588 567 587 jca 
 |-  ( ( b = 0 /\ c = 4 ) -> ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) )
589 547 550 588 jca31 
 |-  ( ( b = 0 /\ c = 4 ) -> ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) )
590 589 olcd 
 |-  ( ( b = 0 /\ c = 4 ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
591 356 464 590 3jaodan 
 |-  ( ( b = 0 /\ ( c = 0 \/ c = 2 \/ c = 4 ) ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
592 359 adantr 
 |-  ( ( b = 2 /\ c = 4 ) -> b =/= 0 )
593 592 neneqd 
 |-  ( ( b = 2 /\ c = 4 ) -> -. b = 0 )
594 593 orcd 
 |-  ( ( b = 2 /\ c = 4 ) -> ( -. b = 0 \/ -. c = 3 ) )
595 582 adantl 
 |-  ( ( b = 2 /\ c = 4 ) -> c =/= 0 )
596 595 neneqd 
 |-  ( ( b = 2 /\ c = 4 ) -> -. c = 0 )
597 596 olcd 
 |-  ( ( b = 2 /\ c = 4 ) -> ( -. b = 3 \/ -. c = 0 ) )
598 593 orcd 
 |-  ( ( b = 2 /\ c = 4 ) -> ( -. b = 0 \/ -. c = 1 ) )
599 596 olcd 
 |-  ( ( b = 2 /\ c = 4 ) -> ( -. b = 1 \/ -. c = 0 ) )
600 598 599 jca 
 |-  ( ( b = 2 /\ c = 4 ) -> ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) )
601 368 adantr 
 |-  ( ( b = 2 /\ c = 4 ) -> b =/= 1 )
602 601 neneqd 
 |-  ( ( b = 2 /\ c = 4 ) -> -. b = 1 )
603 602 orcd 
 |-  ( ( b = 2 /\ c = 4 ) -> ( -. b = 1 \/ -. c = 2 ) )
604 551 adantl 
 |-  ( ( b = 2 /\ c = 4 ) -> c =/= 1 )
605 604 neneqd 
 |-  ( ( b = 2 /\ c = 4 ) -> -. c = 1 )
606 605 olcd 
 |-  ( ( b = 2 /\ c = 4 ) -> ( -. b = 2 \/ -. c = 1 ) )
607 603 606 jca 
 |-  ( ( b = 2 /\ c = 4 ) -> ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) )
608 544 adantl 
 |-  ( ( b = 2 /\ c = 4 ) -> c =/= 3 )
609 608 neneqd 
 |-  ( ( b = 2 /\ c = 4 ) -> -. c = 3 )
610 609 olcd 
 |-  ( ( b = 2 /\ c = 4 ) -> ( -. b = 2 \/ -. c = 3 ) )
611 363 adantr 
 |-  ( ( b = 2 /\ c = 4 ) -> b =/= 3 )
612 611 neneqd 
 |-  ( ( b = 2 /\ c = 4 ) -> -. b = 3 )
613 612 orcd 
 |-  ( ( b = 2 /\ c = 4 ) -> ( -. b = 3 \/ -. c = 2 ) )
614 610 613 jca 
 |-  ( ( b = 2 /\ c = 4 ) -> ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) )
615 600 607 614 3jca 
 |-  ( ( b = 2 /\ c = 4 ) -> ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) )
616 612 orcd 
 |-  ( ( b = 2 /\ c = 4 ) -> ( -. b = 3 \/ -. c = 4 ) )
617 609 olcd 
 |-  ( ( b = 2 /\ c = 4 ) -> ( -. b = 4 \/ -. c = 3 ) )
618 616 617 jca 
 |-  ( ( b = 2 /\ c = 4 ) -> ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) )
619 493 adantr 
 |-  ( ( b = 2 /\ c = 4 ) -> b =/= 4 )
620 619 neneqd 
 |-  ( ( b = 2 /\ c = 4 ) -> -. b = 4 )
621 620 orcd 
 |-  ( ( b = 2 /\ c = 4 ) -> ( -. b = 4 \/ -. c = 5 ) )
622 402 adantr 
 |-  ( ( b = 2 /\ c = 4 ) -> b =/= 5 )
623 622 neneqd 
 |-  ( ( b = 2 /\ c = 4 ) -> -. b = 5 )
624 623 orcd 
 |-  ( ( b = 2 /\ c = 4 ) -> ( -. b = 5 \/ -. c = 4 ) )
625 621 624 jca 
 |-  ( ( b = 2 /\ c = 4 ) -> ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) )
626 593 orcd 
 |-  ( ( b = 2 /\ c = 4 ) -> ( -. b = 0 \/ -. c = 5 ) )
627 596 olcd 
 |-  ( ( b = 2 /\ c = 4 ) -> ( -. b = 5 \/ -. c = 0 ) )
628 626 627 jca 
 |-  ( ( b = 2 /\ c = 4 ) -> ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) )
629 618 625 628 3jca 
 |-  ( ( b = 2 /\ c = 4 ) -> ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) )
630 615 629 jca 
 |-  ( ( b = 2 /\ c = 4 ) -> ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) )
631 594 597 630 jca31 
 |-  ( ( b = 2 /\ c = 4 ) -> ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) )
632 631 olcd 
 |-  ( ( b = 2 /\ c = 4 ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
633 410 509 632 3jaodan 
 |-  ( ( b = 2 /\ ( c = 0 \/ c = 2 \/ c = 4 ) ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
634 446 necon2i 
 |-  ( b = 4 -> b =/= 0 )
635 634 adantr 
 |-  ( ( b = 4 /\ c = 0 ) -> b =/= 0 )
636 635 neneqd 
 |-  ( ( b = 4 /\ c = 0 ) -> -. b = 0 )
637 636 orcd 
 |-  ( ( b = 4 /\ c = 0 ) -> ( -. b = 0 \/ -. c = 3 ) )
638 229 necon2i 
 |-  ( b = 4 -> b =/= 3 )
639 638 adantr 
 |-  ( ( b = 4 /\ c = 0 ) -> b =/= 3 )
640 639 neneqd 
 |-  ( ( b = 4 /\ c = 0 ) -> -. b = 3 )
641 640 orcd 
 |-  ( ( b = 4 /\ c = 0 ) -> ( -. b = 3 \/ -. c = 0 ) )
642 636 orcd 
 |-  ( ( b = 4 /\ c = 0 ) -> ( -. b = 0 \/ -. c = 1 ) )
643 65 necon2i 
 |-  ( b = 4 -> b =/= 1 )
644 643 adantr 
 |-  ( ( b = 4 /\ c = 0 ) -> b =/= 1 )
645 644 neneqd 
 |-  ( ( b = 4 /\ c = 0 ) -> -. b = 1 )
646 645 orcd 
 |-  ( ( b = 4 /\ c = 0 ) -> ( -. b = 1 \/ -. c = 0 ) )
647 642 646 jca 
 |-  ( ( b = 4 /\ c = 0 ) -> ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) )
648 416 necon2i 
 |-  ( c = 0 -> c =/= 2 )
649 648 adantl 
 |-  ( ( b = 4 /\ c = 0 ) -> c =/= 2 )
650 649 neneqd 
 |-  ( ( b = 4 /\ c = 0 ) -> -. c = 2 )
651 650 olcd 
 |-  ( ( b = 4 /\ c = 0 ) -> ( -. b = 1 \/ -. c = 2 ) )
652 374 adantl 
 |-  ( ( b = 4 /\ c = 0 ) -> c =/= 1 )
653 652 neneqd 
 |-  ( ( b = 4 /\ c = 0 ) -> -. c = 1 )
654 653 olcd 
 |-  ( ( b = 4 /\ c = 0 ) -> ( -. b = 2 \/ -. c = 1 ) )
655 651 654 jca 
 |-  ( ( b = 4 /\ c = 0 ) -> ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) )
656 379 adantl 
 |-  ( ( b = 4 /\ c = 0 ) -> c =/= 3 )
657 656 neneqd 
 |-  ( ( b = 4 /\ c = 0 ) -> -. c = 3 )
658 657 olcd 
 |-  ( ( b = 4 /\ c = 0 ) -> ( -. b = 2 \/ -. c = 3 ) )
659 640 orcd 
 |-  ( ( b = 4 /\ c = 0 ) -> ( -. b = 3 \/ -. c = 2 ) )
660 658 659 jca 
 |-  ( ( b = 4 /\ c = 0 ) -> ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) )
661 647 655 660 3jca 
 |-  ( ( b = 4 /\ c = 0 ) -> ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) )
662 640 orcd 
 |-  ( ( b = 4 /\ c = 0 ) -> ( -. b = 3 \/ -. c = 4 ) )
663 657 olcd 
 |-  ( ( b = 4 /\ c = 0 ) -> ( -. b = 4 \/ -. c = 3 ) )
664 662 663 jca 
 |-  ( ( b = 4 /\ c = 0 ) -> ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) )
665 389 adantl 
 |-  ( ( b = 4 /\ c = 0 ) -> c =/= 5 )
666 665 neneqd 
 |-  ( ( b = 4 /\ c = 0 ) -> -. c = 5 )
667 666 olcd 
 |-  ( ( b = 4 /\ c = 0 ) -> ( -. b = 4 \/ -. c = 5 ) )
668 396 adantl 
 |-  ( ( b = 4 /\ c = 0 ) -> c =/= 4 )
669 668 neneqd 
 |-  ( ( b = 4 /\ c = 0 ) -> -. c = 4 )
670 669 olcd 
 |-  ( ( b = 4 /\ c = 0 ) -> ( -. b = 5 \/ -. c = 4 ) )
671 667 670 jca 
 |-  ( ( b = 4 /\ c = 0 ) -> ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) )
672 636 orcd 
 |-  ( ( b = 4 /\ c = 0 ) -> ( -. b = 0 \/ -. c = 5 ) )
673 323 necon2i 
 |-  ( b = 4 -> b =/= 5 )
674 673 adantr 
 |-  ( ( b = 4 /\ c = 0 ) -> b =/= 5 )
675 674 neneqd 
 |-  ( ( b = 4 /\ c = 0 ) -> -. b = 5 )
676 675 orcd 
 |-  ( ( b = 4 /\ c = 0 ) -> ( -. b = 5 \/ -. c = 0 ) )
677 672 676 jca 
 |-  ( ( b = 4 /\ c = 0 ) -> ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) )
678 664 671 677 3jca 
 |-  ( ( b = 4 /\ c = 0 ) -> ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) )
679 661 678 jca 
 |-  ( ( b = 4 /\ c = 0 ) -> ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) )
680 637 641 679 jca31 
 |-  ( ( b = 4 /\ c = 0 ) -> ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) )
681 680 olcd 
 |-  ( ( b = 4 /\ c = 0 ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
682 634 adantr 
 |-  ( ( b = 4 /\ c = 2 ) -> b =/= 0 )
683 682 neneqd 
 |-  ( ( b = 4 /\ c = 2 ) -> -. b = 0 )
684 683 orcd 
 |-  ( ( b = 4 /\ c = 2 ) -> ( -. b = 0 \/ -. c = 3 ) )
685 416 adantl 
 |-  ( ( b = 4 /\ c = 2 ) -> c =/= 0 )
686 685 neneqd 
 |-  ( ( b = 4 /\ c = 2 ) -> -. c = 0 )
687 686 olcd 
 |-  ( ( b = 4 /\ c = 2 ) -> ( -. b = 3 \/ -. c = 0 ) )
688 683 orcd 
 |-  ( ( b = 4 /\ c = 2 ) -> ( -. b = 0 \/ -. c = 1 ) )
689 686 olcd 
 |-  ( ( b = 4 /\ c = 2 ) -> ( -. b = 1 \/ -. c = 0 ) )
690 688 689 jca 
 |-  ( ( b = 4 /\ c = 2 ) -> ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) )
691 643 adantr 
 |-  ( ( b = 4 /\ c = 2 ) -> b =/= 1 )
692 691 neneqd 
 |-  ( ( b = 4 /\ c = 2 ) -> -. b = 1 )
693 692 orcd 
 |-  ( ( b = 4 /\ c = 2 ) -> ( -. b = 1 \/ -. c = 2 ) )
694 420 adantl 
 |-  ( ( b = 4 /\ c = 2 ) -> c =/= 1 )
695 694 neneqd 
 |-  ( ( b = 4 /\ c = 2 ) -> -. c = 1 )
696 695 olcd 
 |-  ( ( b = 4 /\ c = 2 ) -> ( -. b = 2 \/ -. c = 1 ) )
697 693 696 jca 
 |-  ( ( b = 4 /\ c = 2 ) -> ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) )
698 493 necon2i 
 |-  ( b = 4 -> b =/= 2 )
699 698 adantr 
 |-  ( ( b = 4 /\ c = 2 ) -> b =/= 2 )
700 699 neneqd 
 |-  ( ( b = 4 /\ c = 2 ) -> -. b = 2 )
701 700 orcd 
 |-  ( ( b = 4 /\ c = 2 ) -> ( -. b = 2 \/ -. c = 3 ) )
702 638 adantr 
 |-  ( ( b = 4 /\ c = 2 ) -> b =/= 3 )
703 702 neneqd 
 |-  ( ( b = 4 /\ c = 2 ) -> -. b = 3 )
704 703 orcd 
 |-  ( ( b = 4 /\ c = 2 ) -> ( -. b = 3 \/ -. c = 2 ) )
705 701 704 jca 
 |-  ( ( b = 4 /\ c = 2 ) -> ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) )
706 690 697 705 3jca 
 |-  ( ( b = 4 /\ c = 2 ) -> ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) )
707 703 orcd 
 |-  ( ( b = 4 /\ c = 2 ) -> ( -. b = 3 \/ -. c = 4 ) )
708 411 adantl 
 |-  ( ( b = 4 /\ c = 2 ) -> c =/= 3 )
709 708 neneqd 
 |-  ( ( b = 4 /\ c = 2 ) -> -. c = 3 )
710 709 olcd 
 |-  ( ( b = 4 /\ c = 2 ) -> ( -. b = 4 \/ -. c = 3 ) )
711 707 710 jca 
 |-  ( ( b = 4 /\ c = 2 ) -> ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) )
712 455 adantl 
 |-  ( ( b = 4 /\ c = 2 ) -> c =/= 5 )
713 712 neneqd 
 |-  ( ( b = 4 /\ c = 2 ) -> -. c = 5 )
714 713 olcd 
 |-  ( ( b = 4 /\ c = 2 ) -> ( -. b = 4 \/ -. c = 5 ) )
715 neeq1 
 |-  ( c = 2 -> ( c =/= 4 <-> 2 =/= 4 ) )
716 491 715 mpbiri 
 |-  ( c = 2 -> c =/= 4 )
717 716 adantl 
 |-  ( ( b = 4 /\ c = 2 ) -> c =/= 4 )
718 717 neneqd 
 |-  ( ( b = 4 /\ c = 2 ) -> -. c = 4 )
719 718 olcd 
 |-  ( ( b = 4 /\ c = 2 ) -> ( -. b = 5 \/ -. c = 4 ) )
720 714 719 jca 
 |-  ( ( b = 4 /\ c = 2 ) -> ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) )
721 683 orcd 
 |-  ( ( b = 4 /\ c = 2 ) -> ( -. b = 0 \/ -. c = 5 ) )
722 686 olcd 
 |-  ( ( b = 4 /\ c = 2 ) -> ( -. b = 5 \/ -. c = 0 ) )
723 721 722 jca 
 |-  ( ( b = 4 /\ c = 2 ) -> ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) )
724 711 720 723 3jca 
 |-  ( ( b = 4 /\ c = 2 ) -> ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) )
725 706 724 jca 
 |-  ( ( b = 4 /\ c = 2 ) -> ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) )
726 684 687 725 jca31 
 |-  ( ( b = 4 /\ c = 2 ) -> ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) )
727 726 olcd 
 |-  ( ( b = 4 /\ c = 2 ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
728 eqtr3 
 |-  ( ( b = 4 /\ c = 4 ) -> b = c )
729 728 orcd 
 |-  ( ( b = 4 /\ c = 4 ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
730 681 727 729 3jaodan 
 |-  ( ( b = 4 /\ ( c = 0 \/ c = 2 \/ c = 4 ) ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
731 591 633 730 3jaoian 
 |-  ( ( ( b = 0 \/ b = 2 \/ b = 4 ) /\ ( c = 0 \/ c = 2 \/ c = 4 ) ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
732 540 543 731 syl2anb 
 |-  ( ( b e. ( G NeighbVtx 3 ) /\ c e. ( G NeighbVtx 3 ) ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
733 732 rgen2 
 |-  A. b e. ( G NeighbVtx 3 ) A. c e. ( G NeighbVtx 3 ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) )
734 1 2 3 usgrexmpl2nb4 
 |-  ( G NeighbVtx 4 ) = { 3 , 5 }
735 734 eleq2i 
 |-  ( b e. ( G NeighbVtx 4 ) <-> b e. { 3 , 5 } )
736 6 elpr 
 |-  ( b e. { 3 , 5 } <-> ( b = 3 \/ b = 5 ) )
737 735 736 bitri 
 |-  ( b e. ( G NeighbVtx 4 ) <-> ( b = 3 \/ b = 5 ) )
738 734 eleq2i 
 |-  ( c e. ( G NeighbVtx 4 ) <-> c e. { 3 , 5 } )
739 10 elpr 
 |-  ( c e. { 3 , 5 } <-> ( c = 3 \/ c = 5 ) )
740 738 739 bitri 
 |-  ( c e. ( G NeighbVtx 4 ) <-> ( c = 3 \/ c = 5 ) )
741 191 341 243 343 ccase 
 |-  ( ( ( b = 3 \/ b = 5 ) /\ ( c = 3 \/ c = 5 ) ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
742 737 740 741 syl2anb 
 |-  ( ( b e. ( G NeighbVtx 4 ) /\ c e. ( G NeighbVtx 4 ) ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
743 742 rgen2 
 |-  A. b e. ( G NeighbVtx 4 ) A. c e. ( G NeighbVtx 4 ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) )
744 1 2 3 usgrexmpl2nb5 
 |-  ( G NeighbVtx 5 ) = { 0 , 4 }
745 744 eleq2i 
 |-  ( b e. ( G NeighbVtx 5 ) <-> b e. { 0 , 4 } )
746 6 elpr 
 |-  ( b e. { 0 , 4 } <-> ( b = 0 \/ b = 4 ) )
747 745 746 bitri 
 |-  ( b e. ( G NeighbVtx 5 ) <-> ( b = 0 \/ b = 4 ) )
748 744 eleq2i 
 |-  ( c e. ( G NeighbVtx 5 ) <-> c e. { 0 , 4 } )
749 10 elpr 
 |-  ( c e. { 0 , 4 } <-> ( c = 0 \/ c = 4 ) )
750 748 749 bitri 
 |-  ( c e. ( G NeighbVtx 5 ) <-> ( c = 0 \/ c = 4 ) )
751 356 681 590 729 ccase 
 |-  ( ( ( b = 0 \/ b = 4 ) /\ ( c = 0 \/ c = 4 ) ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
752 747 750 751 syl2anb 
 |-  ( ( b e. ( G NeighbVtx 5 ) /\ c e. ( G NeighbVtx 5 ) ) -> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
753 752 rgen2 
 |-  A. b e. ( G NeighbVtx 5 ) A. c e. ( G NeighbVtx 5 ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) )
754 3ex 
 |-  3 e. _V
755 4nn0 
 |-  4 e. NN0
756 755 elexi 
 |-  4 e. _V
757 5nn0 
 |-  5 e. NN0
758 757 elexi 
 |-  5 e. _V
759 oveq2 
 |-  ( a = 3 -> ( G NeighbVtx a ) = ( G NeighbVtx 3 ) )
760 759 raleqdv 
 |-  ( a = 3 -> ( A. c e. ( G NeighbVtx a ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) <-> A. c e. ( G NeighbVtx 3 ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) ) )
761 759 760 raleqbidv 
 |-  ( a = 3 -> ( A. b e. ( G NeighbVtx a ) A. c e. ( G NeighbVtx a ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) <-> A. b e. ( G NeighbVtx 3 ) A. c e. ( G NeighbVtx 3 ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) ) )
762 oveq2 
 |-  ( a = 4 -> ( G NeighbVtx a ) = ( G NeighbVtx 4 ) )
763 762 raleqdv 
 |-  ( a = 4 -> ( A. c e. ( G NeighbVtx a ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) <-> A. c e. ( G NeighbVtx 4 ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) ) )
764 762 763 raleqbidv 
 |-  ( a = 4 -> ( A. b e. ( G NeighbVtx a ) A. c e. ( G NeighbVtx a ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) <-> A. b e. ( G NeighbVtx 4 ) A. c e. ( G NeighbVtx 4 ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) ) )
765 oveq2 
 |-  ( a = 5 -> ( G NeighbVtx a ) = ( G NeighbVtx 5 ) )
766 765 raleqdv 
 |-  ( a = 5 -> ( A. c e. ( G NeighbVtx a ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) <-> A. c e. ( G NeighbVtx 5 ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) ) )
767 765 766 raleqbidv 
 |-  ( a = 5 -> ( A. b e. ( G NeighbVtx a ) A. c e. ( G NeighbVtx a ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) <-> A. b e. ( G NeighbVtx 5 ) A. c e. ( G NeighbVtx 5 ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) ) )
768 754 756 758 761 764 767 raltp 
 |-  ( A. a e. { 3 , 4 , 5 } A. b e. ( G NeighbVtx a ) A. c e. ( G NeighbVtx a ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) <-> ( A. b e. ( G NeighbVtx 3 ) A. c e. ( G NeighbVtx 3 ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) /\ A. b e. ( G NeighbVtx 4 ) A. c e. ( G NeighbVtx 4 ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) /\ A. b e. ( G NeighbVtx 5 ) A. c e. ( G NeighbVtx 5 ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) ) )
769 733 743 753 768 mpbir3an 
 |-  A. a e. { 3 , 4 , 5 } A. b e. ( G NeighbVtx a ) A. c e. ( G NeighbVtx a ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) )
770 ralunb 
 |-  ( A. a e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) A. b e. ( G NeighbVtx a ) A. c e. ( G NeighbVtx a ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) <-> ( A. a e. { 0 , 1 , 2 } A. b e. ( G NeighbVtx a ) A. c e. ( G NeighbVtx a ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) /\ A. a e. { 3 , 4 , 5 } A. b e. ( G NeighbVtx a ) A. c e. ( G NeighbVtx a ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) ) )
771 536 769 770 mpbir2an 
 |-  A. a e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) A. b e. ( G NeighbVtx a ) A. c e. ( G NeighbVtx a ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) )
772 ianor 
 |-  ( -. ( b =/= c /\ { b , c } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) ) <-> ( -. b =/= c \/ -. { b , c } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) ) )
773 nne 
 |-  ( -. b =/= c <-> b = c )
774 ioran 
 |-  ( -. ( ( ( b = 0 /\ c = 3 ) \/ ( b = 3 /\ c = 0 ) ) \/ ( ( ( ( b = 0 /\ c = 1 ) \/ ( b = 1 /\ c = 0 ) ) \/ ( ( b = 1 /\ c = 2 ) \/ ( b = 2 /\ c = 1 ) ) \/ ( ( b = 2 /\ c = 3 ) \/ ( b = 3 /\ c = 2 ) ) ) \/ ( ( ( b = 3 /\ c = 4 ) \/ ( b = 4 /\ c = 3 ) ) \/ ( ( b = 4 /\ c = 5 ) \/ ( b = 5 /\ c = 4 ) ) \/ ( ( b = 0 /\ c = 5 ) \/ ( b = 5 /\ c = 0 ) ) ) ) ) <-> ( -. ( ( b = 0 /\ c = 3 ) \/ ( b = 3 /\ c = 0 ) ) /\ -. ( ( ( ( b = 0 /\ c = 1 ) \/ ( b = 1 /\ c = 0 ) ) \/ ( ( b = 1 /\ c = 2 ) \/ ( b = 2 /\ c = 1 ) ) \/ ( ( b = 2 /\ c = 3 ) \/ ( b = 3 /\ c = 2 ) ) ) \/ ( ( ( b = 3 /\ c = 4 ) \/ ( b = 4 /\ c = 3 ) ) \/ ( ( b = 4 /\ c = 5 ) \/ ( b = 5 /\ c = 4 ) ) \/ ( ( b = 0 /\ c = 5 ) \/ ( b = 5 /\ c = 0 ) ) ) ) ) )
775 ioran 
 |-  ( -. ( ( b = 0 /\ c = 3 ) \/ ( b = 3 /\ c = 0 ) ) <-> ( -. ( b = 0 /\ c = 3 ) /\ -. ( b = 3 /\ c = 0 ) ) )
776 ianor 
 |-  ( -. ( b = 0 /\ c = 3 ) <-> ( -. b = 0 \/ -. c = 3 ) )
777 ianor 
 |-  ( -. ( b = 3 /\ c = 0 ) <-> ( -. b = 3 \/ -. c = 0 ) )
778 776 777 anbi12i 
 |-  ( ( -. ( b = 0 /\ c = 3 ) /\ -. ( b = 3 /\ c = 0 ) ) <-> ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) )
779 775 778 bitri 
 |-  ( -. ( ( b = 0 /\ c = 3 ) \/ ( b = 3 /\ c = 0 ) ) <-> ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) )
780 ioran 
 |-  ( -. ( ( ( ( b = 0 /\ c = 1 ) \/ ( b = 1 /\ c = 0 ) ) \/ ( ( b = 1 /\ c = 2 ) \/ ( b = 2 /\ c = 1 ) ) \/ ( ( b = 2 /\ c = 3 ) \/ ( b = 3 /\ c = 2 ) ) ) \/ ( ( ( b = 3 /\ c = 4 ) \/ ( b = 4 /\ c = 3 ) ) \/ ( ( b = 4 /\ c = 5 ) \/ ( b = 5 /\ c = 4 ) ) \/ ( ( b = 0 /\ c = 5 ) \/ ( b = 5 /\ c = 0 ) ) ) ) <-> ( -. ( ( ( b = 0 /\ c = 1 ) \/ ( b = 1 /\ c = 0 ) ) \/ ( ( b = 1 /\ c = 2 ) \/ ( b = 2 /\ c = 1 ) ) \/ ( ( b = 2 /\ c = 3 ) \/ ( b = 3 /\ c = 2 ) ) ) /\ -. ( ( ( b = 3 /\ c = 4 ) \/ ( b = 4 /\ c = 3 ) ) \/ ( ( b = 4 /\ c = 5 ) \/ ( b = 5 /\ c = 4 ) ) \/ ( ( b = 0 /\ c = 5 ) \/ ( b = 5 /\ c = 0 ) ) ) ) )
781 3ioran 
 |-  ( -. ( ( ( b = 0 /\ c = 1 ) \/ ( b = 1 /\ c = 0 ) ) \/ ( ( b = 1 /\ c = 2 ) \/ ( b = 2 /\ c = 1 ) ) \/ ( ( b = 2 /\ c = 3 ) \/ ( b = 3 /\ c = 2 ) ) ) <-> ( -. ( ( b = 0 /\ c = 1 ) \/ ( b = 1 /\ c = 0 ) ) /\ -. ( ( b = 1 /\ c = 2 ) \/ ( b = 2 /\ c = 1 ) ) /\ -. ( ( b = 2 /\ c = 3 ) \/ ( b = 3 /\ c = 2 ) ) ) )
782 ioran 
 |-  ( -. ( ( b = 0 /\ c = 1 ) \/ ( b = 1 /\ c = 0 ) ) <-> ( -. ( b = 0 /\ c = 1 ) /\ -. ( b = 1 /\ c = 0 ) ) )
783 ianor 
 |-  ( -. ( b = 0 /\ c = 1 ) <-> ( -. b = 0 \/ -. c = 1 ) )
784 ianor 
 |-  ( -. ( b = 1 /\ c = 0 ) <-> ( -. b = 1 \/ -. c = 0 ) )
785 783 784 anbi12i 
 |-  ( ( -. ( b = 0 /\ c = 1 ) /\ -. ( b = 1 /\ c = 0 ) ) <-> ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) )
786 782 785 bitri 
 |-  ( -. ( ( b = 0 /\ c = 1 ) \/ ( b = 1 /\ c = 0 ) ) <-> ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) )
787 ioran 
 |-  ( -. ( ( b = 1 /\ c = 2 ) \/ ( b = 2 /\ c = 1 ) ) <-> ( -. ( b = 1 /\ c = 2 ) /\ -. ( b = 2 /\ c = 1 ) ) )
788 ianor 
 |-  ( -. ( b = 1 /\ c = 2 ) <-> ( -. b = 1 \/ -. c = 2 ) )
789 ianor 
 |-  ( -. ( b = 2 /\ c = 1 ) <-> ( -. b = 2 \/ -. c = 1 ) )
790 788 789 anbi12i 
 |-  ( ( -. ( b = 1 /\ c = 2 ) /\ -. ( b = 2 /\ c = 1 ) ) <-> ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) )
791 787 790 bitri 
 |-  ( -. ( ( b = 1 /\ c = 2 ) \/ ( b = 2 /\ c = 1 ) ) <-> ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) )
792 ioran 
 |-  ( -. ( ( b = 2 /\ c = 3 ) \/ ( b = 3 /\ c = 2 ) ) <-> ( -. ( b = 2 /\ c = 3 ) /\ -. ( b = 3 /\ c = 2 ) ) )
793 ianor 
 |-  ( -. ( b = 2 /\ c = 3 ) <-> ( -. b = 2 \/ -. c = 3 ) )
794 ianor 
 |-  ( -. ( b = 3 /\ c = 2 ) <-> ( -. b = 3 \/ -. c = 2 ) )
795 793 794 anbi12i 
 |-  ( ( -. ( b = 2 /\ c = 3 ) /\ -. ( b = 3 /\ c = 2 ) ) <-> ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) )
796 792 795 bitri 
 |-  ( -. ( ( b = 2 /\ c = 3 ) \/ ( b = 3 /\ c = 2 ) ) <-> ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) )
797 786 791 796 3anbi123i 
 |-  ( ( -. ( ( b = 0 /\ c = 1 ) \/ ( b = 1 /\ c = 0 ) ) /\ -. ( ( b = 1 /\ c = 2 ) \/ ( b = 2 /\ c = 1 ) ) /\ -. ( ( b = 2 /\ c = 3 ) \/ ( b = 3 /\ c = 2 ) ) ) <-> ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) )
798 781 797 bitri 
 |-  ( -. ( ( ( b = 0 /\ c = 1 ) \/ ( b = 1 /\ c = 0 ) ) \/ ( ( b = 1 /\ c = 2 ) \/ ( b = 2 /\ c = 1 ) ) \/ ( ( b = 2 /\ c = 3 ) \/ ( b = 3 /\ c = 2 ) ) ) <-> ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) )
799 3ioran 
 |-  ( -. ( ( ( b = 3 /\ c = 4 ) \/ ( b = 4 /\ c = 3 ) ) \/ ( ( b = 4 /\ c = 5 ) \/ ( b = 5 /\ c = 4 ) ) \/ ( ( b = 0 /\ c = 5 ) \/ ( b = 5 /\ c = 0 ) ) ) <-> ( -. ( ( b = 3 /\ c = 4 ) \/ ( b = 4 /\ c = 3 ) ) /\ -. ( ( b = 4 /\ c = 5 ) \/ ( b = 5 /\ c = 4 ) ) /\ -. ( ( b = 0 /\ c = 5 ) \/ ( b = 5 /\ c = 0 ) ) ) )
800 ioran 
 |-  ( -. ( ( b = 3 /\ c = 4 ) \/ ( b = 4 /\ c = 3 ) ) <-> ( -. ( b = 3 /\ c = 4 ) /\ -. ( b = 4 /\ c = 3 ) ) )
801 ianor 
 |-  ( -. ( b = 3 /\ c = 4 ) <-> ( -. b = 3 \/ -. c = 4 ) )
802 ianor 
 |-  ( -. ( b = 4 /\ c = 3 ) <-> ( -. b = 4 \/ -. c = 3 ) )
803 801 802 anbi12i 
 |-  ( ( -. ( b = 3 /\ c = 4 ) /\ -. ( b = 4 /\ c = 3 ) ) <-> ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) )
804 800 803 bitri 
 |-  ( -. ( ( b = 3 /\ c = 4 ) \/ ( b = 4 /\ c = 3 ) ) <-> ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) )
805 ioran 
 |-  ( -. ( ( b = 4 /\ c = 5 ) \/ ( b = 5 /\ c = 4 ) ) <-> ( -. ( b = 4 /\ c = 5 ) /\ -. ( b = 5 /\ c = 4 ) ) )
806 ianor 
 |-  ( -. ( b = 4 /\ c = 5 ) <-> ( -. b = 4 \/ -. c = 5 ) )
807 ianor 
 |-  ( -. ( b = 5 /\ c = 4 ) <-> ( -. b = 5 \/ -. c = 4 ) )
808 806 807 anbi12i 
 |-  ( ( -. ( b = 4 /\ c = 5 ) /\ -. ( b = 5 /\ c = 4 ) ) <-> ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) )
809 805 808 bitri 
 |-  ( -. ( ( b = 4 /\ c = 5 ) \/ ( b = 5 /\ c = 4 ) ) <-> ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) )
810 ioran 
 |-  ( -. ( ( b = 0 /\ c = 5 ) \/ ( b = 5 /\ c = 0 ) ) <-> ( -. ( b = 0 /\ c = 5 ) /\ -. ( b = 5 /\ c = 0 ) ) )
811 ianor 
 |-  ( -. ( b = 0 /\ c = 5 ) <-> ( -. b = 0 \/ -. c = 5 ) )
812 ianor 
 |-  ( -. ( b = 5 /\ c = 0 ) <-> ( -. b = 5 \/ -. c = 0 ) )
813 811 812 anbi12i 
 |-  ( ( -. ( b = 0 /\ c = 5 ) /\ -. ( b = 5 /\ c = 0 ) ) <-> ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) )
814 810 813 bitri 
 |-  ( -. ( ( b = 0 /\ c = 5 ) \/ ( b = 5 /\ c = 0 ) ) <-> ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) )
815 804 809 814 3anbi123i 
 |-  ( ( -. ( ( b = 3 /\ c = 4 ) \/ ( b = 4 /\ c = 3 ) ) /\ -. ( ( b = 4 /\ c = 5 ) \/ ( b = 5 /\ c = 4 ) ) /\ -. ( ( b = 0 /\ c = 5 ) \/ ( b = 5 /\ c = 0 ) ) ) <-> ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) )
816 799 815 bitri 
 |-  ( -. ( ( ( b = 3 /\ c = 4 ) \/ ( b = 4 /\ c = 3 ) ) \/ ( ( b = 4 /\ c = 5 ) \/ ( b = 5 /\ c = 4 ) ) \/ ( ( b = 0 /\ c = 5 ) \/ ( b = 5 /\ c = 0 ) ) ) <-> ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) )
817 798 816 anbi12i 
 |-  ( ( -. ( ( ( b = 0 /\ c = 1 ) \/ ( b = 1 /\ c = 0 ) ) \/ ( ( b = 1 /\ c = 2 ) \/ ( b = 2 /\ c = 1 ) ) \/ ( ( b = 2 /\ c = 3 ) \/ ( b = 3 /\ c = 2 ) ) ) /\ -. ( ( ( b = 3 /\ c = 4 ) \/ ( b = 4 /\ c = 3 ) ) \/ ( ( b = 4 /\ c = 5 ) \/ ( b = 5 /\ c = 4 ) ) \/ ( ( b = 0 /\ c = 5 ) \/ ( b = 5 /\ c = 0 ) ) ) ) <-> ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) )
818 780 817 bitri 
 |-  ( -. ( ( ( ( b = 0 /\ c = 1 ) \/ ( b = 1 /\ c = 0 ) ) \/ ( ( b = 1 /\ c = 2 ) \/ ( b = 2 /\ c = 1 ) ) \/ ( ( b = 2 /\ c = 3 ) \/ ( b = 3 /\ c = 2 ) ) ) \/ ( ( ( b = 3 /\ c = 4 ) \/ ( b = 4 /\ c = 3 ) ) \/ ( ( b = 4 /\ c = 5 ) \/ ( b = 5 /\ c = 4 ) ) \/ ( ( b = 0 /\ c = 5 ) \/ ( b = 5 /\ c = 0 ) ) ) ) <-> ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) )
819 779 818 anbi12i 
 |-  ( ( -. ( ( b = 0 /\ c = 3 ) \/ ( b = 3 /\ c = 0 ) ) /\ -. ( ( ( ( b = 0 /\ c = 1 ) \/ ( b = 1 /\ c = 0 ) ) \/ ( ( b = 1 /\ c = 2 ) \/ ( b = 2 /\ c = 1 ) ) \/ ( ( b = 2 /\ c = 3 ) \/ ( b = 3 /\ c = 2 ) ) ) \/ ( ( ( b = 3 /\ c = 4 ) \/ ( b = 4 /\ c = 3 ) ) \/ ( ( b = 4 /\ c = 5 ) \/ ( b = 5 /\ c = 4 ) ) \/ ( ( b = 0 /\ c = 5 ) \/ ( b = 5 /\ c = 0 ) ) ) ) ) <-> ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) )
820 774 819 bitri 
 |-  ( -. ( ( ( b = 0 /\ c = 3 ) \/ ( b = 3 /\ c = 0 ) ) \/ ( ( ( ( b = 0 /\ c = 1 ) \/ ( b = 1 /\ c = 0 ) ) \/ ( ( b = 1 /\ c = 2 ) \/ ( b = 2 /\ c = 1 ) ) \/ ( ( b = 2 /\ c = 3 ) \/ ( b = 3 /\ c = 2 ) ) ) \/ ( ( ( b = 3 /\ c = 4 ) \/ ( b = 4 /\ c = 3 ) ) \/ ( ( b = 4 /\ c = 5 ) \/ ( b = 5 /\ c = 4 ) ) \/ ( ( b = 0 /\ c = 5 ) \/ ( b = 5 /\ c = 0 ) ) ) ) ) <-> ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) )
821 6 10 523 524 preq12b 
 |-  ( { b , c } = { 0 , 1 } <-> ( ( b = 0 /\ c = 1 ) \/ ( b = 1 /\ c = 0 ) ) )
822 6 10 524 525 preq12b 
 |-  ( { b , c } = { 1 , 2 } <-> ( ( b = 1 /\ c = 2 ) \/ ( b = 2 /\ c = 1 ) ) )
823 6 10 525 754 preq12b 
 |-  ( { b , c } = { 2 , 3 } <-> ( ( b = 2 /\ c = 3 ) \/ ( b = 3 /\ c = 2 ) ) )
824 821 822 823 3orbi123i 
 |-  ( ( { b , c } = { 0 , 1 } \/ { b , c } = { 1 , 2 } \/ { b , c } = { 2 , 3 } ) <-> ( ( ( b = 0 /\ c = 1 ) \/ ( b = 1 /\ c = 0 ) ) \/ ( ( b = 1 /\ c = 2 ) \/ ( b = 2 /\ c = 1 ) ) \/ ( ( b = 2 /\ c = 3 ) \/ ( b = 3 /\ c = 2 ) ) ) )
825 6 10 754 756 preq12b 
 |-  ( { b , c } = { 3 , 4 } <-> ( ( b = 3 /\ c = 4 ) \/ ( b = 4 /\ c = 3 ) ) )
826 6 10 756 758 preq12b 
 |-  ( { b , c } = { 4 , 5 } <-> ( ( b = 4 /\ c = 5 ) \/ ( b = 5 /\ c = 4 ) ) )
827 6 10 523 758 preq12b 
 |-  ( { b , c } = { 0 , 5 } <-> ( ( b = 0 /\ c = 5 ) \/ ( b = 5 /\ c = 0 ) ) )
828 825 826 827 3orbi123i 
 |-  ( ( { b , c } = { 3 , 4 } \/ { b , c } = { 4 , 5 } \/ { b , c } = { 0 , 5 } ) <-> ( ( ( b = 3 /\ c = 4 ) \/ ( b = 4 /\ c = 3 ) ) \/ ( ( b = 4 /\ c = 5 ) \/ ( b = 5 /\ c = 4 ) ) \/ ( ( b = 0 /\ c = 5 ) \/ ( b = 5 /\ c = 0 ) ) ) )
829 824 828 orbi12i 
 |-  ( ( ( { b , c } = { 0 , 1 } \/ { b , c } = { 1 , 2 } \/ { b , c } = { 2 , 3 } ) \/ ( { b , c } = { 3 , 4 } \/ { b , c } = { 4 , 5 } \/ { b , c } = { 0 , 5 } ) ) <-> ( ( ( ( b = 0 /\ c = 1 ) \/ ( b = 1 /\ c = 0 ) ) \/ ( ( b = 1 /\ c = 2 ) \/ ( b = 2 /\ c = 1 ) ) \/ ( ( b = 2 /\ c = 3 ) \/ ( b = 3 /\ c = 2 ) ) ) \/ ( ( ( b = 3 /\ c = 4 ) \/ ( b = 4 /\ c = 3 ) ) \/ ( ( b = 4 /\ c = 5 ) \/ ( b = 5 /\ c = 4 ) ) \/ ( ( b = 0 /\ c = 5 ) \/ ( b = 5 /\ c = 0 ) ) ) ) )
830 829 orbi2i 
 |-  ( ( ( ( b = 0 /\ c = 3 ) \/ ( b = 3 /\ c = 0 ) ) \/ ( ( { b , c } = { 0 , 1 } \/ { b , c } = { 1 , 2 } \/ { b , c } = { 2 , 3 } ) \/ ( { b , c } = { 3 , 4 } \/ { b , c } = { 4 , 5 } \/ { b , c } = { 0 , 5 } ) ) ) <-> ( ( ( b = 0 /\ c = 3 ) \/ ( b = 3 /\ c = 0 ) ) \/ ( ( ( ( b = 0 /\ c = 1 ) \/ ( b = 1 /\ c = 0 ) ) \/ ( ( b = 1 /\ c = 2 ) \/ ( b = 2 /\ c = 1 ) ) \/ ( ( b = 2 /\ c = 3 ) \/ ( b = 3 /\ c = 2 ) ) ) \/ ( ( ( b = 3 /\ c = 4 ) \/ ( b = 4 /\ c = 3 ) ) \/ ( ( b = 4 /\ c = 5 ) \/ ( b = 5 /\ c = 4 ) ) \/ ( ( b = 0 /\ c = 5 ) \/ ( b = 5 /\ c = 0 ) ) ) ) ) )
831 820 830 xchnxbir 
 |-  ( -. ( ( ( b = 0 /\ c = 3 ) \/ ( b = 3 /\ c = 0 ) ) \/ ( ( { b , c } = { 0 , 1 } \/ { b , c } = { 1 , 2 } \/ { b , c } = { 2 , 3 } ) \/ ( { b , c } = { 3 , 4 } \/ { b , c } = { 4 , 5 } \/ { b , c } = { 0 , 5 } ) ) ) <-> ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) )
832 elun 
 |-  ( { b , c } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) <-> ( { b , c } e. { { 0 , 3 } } \/ { b , c } e. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) )
833 prex 
 |-  { b , c } e. _V
834 833 elsn 
 |-  ( { b , c } e. { { 0 , 3 } } <-> { b , c } = { 0 , 3 } )
835 6 10 523 754 preq12b 
 |-  ( { b , c } = { 0 , 3 } <-> ( ( b = 0 /\ c = 3 ) \/ ( b = 3 /\ c = 0 ) ) )
836 834 835 bitri 
 |-  ( { b , c } e. { { 0 , 3 } } <-> ( ( b = 0 /\ c = 3 ) \/ ( b = 3 /\ c = 0 ) ) )
837 elun 
 |-  ( { b , c } e. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) <-> ( { b , c } e. { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } \/ { b , c } e. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) )
838 833 eltp 
 |-  ( { b , c } e. { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } <-> ( { b , c } = { 0 , 1 } \/ { b , c } = { 1 , 2 } \/ { b , c } = { 2 , 3 } ) )
839 833 eltp 
 |-  ( { b , c } e. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } <-> ( { b , c } = { 3 , 4 } \/ { b , c } = { 4 , 5 } \/ { b , c } = { 0 , 5 } ) )
840 838 839 orbi12i 
 |-  ( ( { b , c } e. { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } \/ { b , c } e. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) <-> ( ( { b , c } = { 0 , 1 } \/ { b , c } = { 1 , 2 } \/ { b , c } = { 2 , 3 } ) \/ ( { b , c } = { 3 , 4 } \/ { b , c } = { 4 , 5 } \/ { b , c } = { 0 , 5 } ) ) )
841 837 840 bitri 
 |-  ( { b , c } e. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) <-> ( ( { b , c } = { 0 , 1 } \/ { b , c } = { 1 , 2 } \/ { b , c } = { 2 , 3 } ) \/ ( { b , c } = { 3 , 4 } \/ { b , c } = { 4 , 5 } \/ { b , c } = { 0 , 5 } ) ) )
842 836 841 orbi12i 
 |-  ( ( { b , c } e. { { 0 , 3 } } \/ { b , c } e. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) <-> ( ( ( b = 0 /\ c = 3 ) \/ ( b = 3 /\ c = 0 ) ) \/ ( ( { b , c } = { 0 , 1 } \/ { b , c } = { 1 , 2 } \/ { b , c } = { 2 , 3 } ) \/ ( { b , c } = { 3 , 4 } \/ { b , c } = { 4 , 5 } \/ { b , c } = { 0 , 5 } ) ) ) )
843 832 842 bitri 
 |-  ( { b , c } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) <-> ( ( ( b = 0 /\ c = 3 ) \/ ( b = 3 /\ c = 0 ) ) \/ ( ( { b , c } = { 0 , 1 } \/ { b , c } = { 1 , 2 } \/ { b , c } = { 2 , 3 } ) \/ ( { b , c } = { 3 , 4 } \/ { b , c } = { 4 , 5 } \/ { b , c } = { 0 , 5 } ) ) ) )
844 831 843 xchnxbir 
 |-  ( -. { b , c } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) <-> ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) )
845 773 844 orbi12i 
 |-  ( ( -. b =/= c \/ -. { b , c } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) ) <-> ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) )
846 772 845 bitr2i 
 |-  ( ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) <-> -. ( b =/= c /\ { b , c } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) ) )
847 846 3ralbii 
 |-  ( A. a e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) A. b e. ( G NeighbVtx a ) A. c e. ( G NeighbVtx a ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) <-> A. a e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) A. b e. ( G NeighbVtx a ) A. c e. ( G NeighbVtx a ) -. ( b =/= c /\ { b , c } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) ) )
848 ralnex3 
 |-  ( A. a e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) A. b e. ( G NeighbVtx a ) A. c e. ( G NeighbVtx a ) -. ( b =/= c /\ { b , c } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) ) <-> -. E. a e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) E. b e. ( G NeighbVtx a ) E. c e. ( G NeighbVtx a ) ( b =/= c /\ { b , c } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) ) )
849 847 848 bitri 
 |-  ( A. a e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) A. b e. ( G NeighbVtx a ) A. c e. ( G NeighbVtx a ) ( b = c \/ ( ( ( -. b = 0 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 0 ) ) /\ ( ( ( ( -. b = 0 \/ -. c = 1 ) /\ ( -. b = 1 \/ -. c = 0 ) ) /\ ( ( -. b = 1 \/ -. c = 2 ) /\ ( -. b = 2 \/ -. c = 1 ) ) /\ ( ( -. b = 2 \/ -. c = 3 ) /\ ( -. b = 3 \/ -. c = 2 ) ) ) /\ ( ( ( -. b = 3 \/ -. c = 4 ) /\ ( -. b = 4 \/ -. c = 3 ) ) /\ ( ( -. b = 4 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 4 ) ) /\ ( ( -. b = 0 \/ -. c = 5 ) /\ ( -. b = 5 \/ -. c = 0 ) ) ) ) ) ) <-> -. E. a e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) E. b e. ( G NeighbVtx a ) E. c e. ( G NeighbVtx a ) ( b =/= c /\ { b , c } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) ) )
850 771 849 mpbi 
 |-  -. E. a e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) E. b e. ( G NeighbVtx a ) E. c e. ( G NeighbVtx a ) ( b =/= c /\ { b , c } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) )
851 1 2 3 usgrexmpl2 
 |-  G e. USGraph
852 1 2 3 usgrexmpl2vtx 
 |-  ( Vtx ` G ) = ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } )
853 852 eqcomi 
 |-  ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) = ( Vtx ` G )
854 1 2 3 usgrexmpl2edg 
 |-  ( Edg ` G ) = ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) )
855 854 eqcomi 
 |-  ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) = ( Edg ` G )
856 eqid 
 |-  ( G NeighbVtx a ) = ( G NeighbVtx a )
857 853 855 856 usgrgrtrirex 
 |-  ( G e. USGraph -> ( E. t t e. ( GrTriangles ` G ) <-> E. a e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) E. b e. ( G NeighbVtx a ) E. c e. ( G NeighbVtx a ) ( b =/= c /\ { b , c } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) ) ) )
858 851 857 ax-mp 
 |-  ( E. t t e. ( GrTriangles ` G ) <-> E. a e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) E. b e. ( G NeighbVtx a ) E. c e. ( G NeighbVtx a ) ( b =/= c /\ { b , c } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) ) )
859 850 858 mtbir 
 |-  -. E. t t e. ( GrTriangles ` G )