usgrexmpl2trifr

	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 )

Metamath Proof Explorer

Theorem usgrexmpl2trifr

Proof