Proof of Theorem nb3grapr2
Step | Hyp | Ref
| Expression |
1 | | 3anan32 1043 |
. . . . 5
⊢ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ↔ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ {𝐵, 𝐶} ∈ ran 𝐸)) |
2 | 1 | a1i 11 |
. . . 4
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ↔ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ {𝐵, 𝐶} ∈ ran 𝐸))) |
3 | | prcom 4211 |
. . . . . . . . . . 11
⊢ {𝐶, 𝐴} = {𝐴, 𝐶} |
4 | 3 | eleq1i 2679 |
. . . . . . . . . 10
⊢ ({𝐶, 𝐴} ∈ ran 𝐸 ↔ {𝐴, 𝐶} ∈ ran 𝐸) |
5 | 4 | biimpi 205 |
. . . . . . . . 9
⊢ ({𝐶, 𝐴} ∈ ran 𝐸 → {𝐴, 𝐶} ∈ ran 𝐸) |
6 | 5 | pm4.71i 662 |
. . . . . . . 8
⊢ ({𝐶, 𝐴} ∈ ran 𝐸 ↔ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸)) |
7 | 6 | anbi2i 726 |
. . . . . . 7
⊢ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸))) |
8 | | anass 679 |
. . . . . . 7
⊢ ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ {𝐴, 𝐶} ∈ ran 𝐸) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸))) |
9 | 7, 8 | bitr4i 266 |
. . . . . 6
⊢ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ↔ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ {𝐴, 𝐶} ∈ ran 𝐸)) |
10 | 9 | anbi1i 727 |
. . . . 5
⊢ ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ {𝐵, 𝐶} ∈ ran 𝐸) ↔ ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ {𝐵, 𝐶} ∈ ran 𝐸)) |
11 | | anass 679 |
. . . . 5
⊢
(((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ {𝐵, 𝐶} ∈ ran 𝐸) ↔ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))) |
12 | 10, 11 | bitri 263 |
. . . 4
⊢ ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ {𝐵, 𝐶} ∈ ran 𝐸) ↔ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))) |
13 | 2, 12 | syl6bb 275 |
. . 3
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ↔ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)))) |
14 | | prcom 4211 |
. . . . . . . . . 10
⊢ {𝐴, 𝐵} = {𝐵, 𝐴} |
15 | 14 | eleq1i 2679 |
. . . . . . . . 9
⊢ ({𝐴, 𝐵} ∈ ran 𝐸 ↔ {𝐵, 𝐴} ∈ ran 𝐸) |
16 | 15 | biimpi 205 |
. . . . . . . 8
⊢ ({𝐴, 𝐵} ∈ ran 𝐸 → {𝐵, 𝐴} ∈ ran 𝐸) |
17 | 16 | pm4.71i 662 |
. . . . . . 7
⊢ ({𝐴, 𝐵} ∈ ran 𝐸 ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸)) |
18 | 17 | anbi1i 727 |
. . . . . 6
⊢ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ↔ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸) ∧ {𝐶, 𝐴} ∈ ran 𝐸)) |
19 | | df-3an 1033 |
. . . . . 6
⊢ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ↔ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸) ∧ {𝐶, 𝐴} ∈ ran 𝐸)) |
20 | 18, 19 | bitr4i 266 |
. . . . 5
⊢ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸)) |
21 | | prcom 4211 |
. . . . . . . . . 10
⊢ {𝐵, 𝐶} = {𝐶, 𝐵} |
22 | 21 | eleq1i 2679 |
. . . . . . . . 9
⊢ ({𝐵, 𝐶} ∈ ran 𝐸 ↔ {𝐶, 𝐵} ∈ ran 𝐸) |
23 | 22 | biimpi 205 |
. . . . . . . 8
⊢ ({𝐵, 𝐶} ∈ ran 𝐸 → {𝐶, 𝐵} ∈ ran 𝐸) |
24 | 23 | pm4.71i 662 |
. . . . . . 7
⊢ ({𝐵, 𝐶} ∈ ran 𝐸 ↔ ({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)) |
25 | 24 | anbi2i 726 |
. . . . . 6
⊢ (({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ↔ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ ({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
26 | | 3anass 1035 |
. . . . . 6
⊢ (({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸) ↔ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ ({𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
27 | 25, 26 | bitr4i 266 |
. . . . 5
⊢ (({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ↔ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)) |
28 | 20, 27 | anbi12i 729 |
. . . 4
⊢ ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) ↔ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
29 | | an6 1400 |
. . . 4
⊢ ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)) ↔ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
30 | 28, 29 | bitri 263 |
. . 3
⊢ ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ∧ ({𝐴, 𝐶} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸)) ↔ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
31 | 13, 30 | syl6bb 275 |
. 2
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ↔ (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)))) |
32 | | nb3graprlem1 25980 |
. . . . 5
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ↔ ({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸))) |
33 | 32 | bicomd 212 |
. . . 4
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ↔ (〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶})) |
34 | | 3ancoma 1038 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ↔ (𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍)) |
35 | 34 | biimpi 205 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍)) |
36 | | tpcoma 4229 |
. . . . . . . . 9
⊢ {𝐴, 𝐵, 𝐶} = {𝐵, 𝐴, 𝐶} |
37 | 36 | eqeq2i 2622 |
. . . . . . . 8
⊢ (𝑉 = {𝐴, 𝐵, 𝐶} ↔ 𝑉 = {𝐵, 𝐴, 𝐶}) |
38 | 37 | biimpi 205 |
. . . . . . 7
⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐵, 𝐴, 𝐶}) |
39 | 38 | anim1i 590 |
. . . . . 6
⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → (𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝑉 USGrph 𝐸)) |
40 | | nb3graprlem1 25980 |
. . . . . 6
⊢ (((𝐵 ∈ 𝑌 ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐵, 𝐴, 𝐶} ∧ 𝑉 USGrph 𝐸)) → ((〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝐴, 𝐶} ↔ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))) |
41 | 35, 39, 40 | syl2an 493 |
. . . . 5
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → ((〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝐴, 𝐶} ↔ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸))) |
42 | 41 | bicomd 212 |
. . . 4
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → (({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ↔ (〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝐴, 𝐶})) |
43 | | 3anrot 1036 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍)) |
44 | 43 | biimpri 217 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) → (𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) |
45 | | tprot 4228 |
. . . . . . . . . 10
⊢ {𝐶, 𝐴, 𝐵} = {𝐴, 𝐵, 𝐶} |
46 | 45 | eqcomi 2619 |
. . . . . . . . 9
⊢ {𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵} |
47 | 46 | eqeq2i 2622 |
. . . . . . . 8
⊢ (𝑉 = {𝐴, 𝐵, 𝐶} ↔ 𝑉 = {𝐶, 𝐴, 𝐵}) |
48 | 47 | biimpi 205 |
. . . . . . 7
⊢ (𝑉 = {𝐴, 𝐵, 𝐶} → 𝑉 = {𝐶, 𝐴, 𝐵}) |
49 | 48 | anim1i 590 |
. . . . . 6
⊢ ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → (𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝑉 USGrph 𝐸)) |
50 | | nb3graprlem1 25980 |
. . . . . 6
⊢ (((𝐶 ∈ 𝑍 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ (𝑉 = {𝐶, 𝐴, 𝐵} ∧ 𝑉 USGrph 𝐸)) → ((〈𝑉, 𝐸〉 Neighbors 𝐶) = {𝐴, 𝐵} ↔ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
51 | 44, 49, 50 | syl2an 493 |
. . . . 5
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → ((〈𝑉, 𝐸〉 Neighbors 𝐶) = {𝐴, 𝐵} ↔ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸))) |
52 | 51 | bicomd 212 |
. . . 4
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → (({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸) ↔ (〈𝑉, 𝐸〉 Neighbors 𝐶) = {𝐴, 𝐵})) |
53 | 33, 42, 52 | 3anbi123d 1391 |
. . 3
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)) ↔ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∧ (〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝐴, 𝐶} ∧ (〈𝑉, 𝐸〉 Neighbors 𝐶) = {𝐴, 𝐵}))) |
54 | 53 | 3adant3 1074 |
. 2
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐴, 𝐶} ∈ ran 𝐸) ∧ ({𝐵, 𝐴} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸) ∧ ({𝐶, 𝐴} ∈ ran 𝐸 ∧ {𝐶, 𝐵} ∈ ran 𝐸)) ↔ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∧ (〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝐴, 𝐶} ∧ (〈𝑉, 𝐸〉 Neighbors 𝐶) = {𝐴, 𝐵}))) |
55 | 31, 54 | bitrd 267 |
1
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → (({𝐴, 𝐵} ∈ ran 𝐸 ∧ {𝐵, 𝐶} ∈ ran 𝐸 ∧ {𝐶, 𝐴} ∈ ran 𝐸) ↔ ((〈𝑉, 𝐸〉 Neighbors 𝐴) = {𝐵, 𝐶} ∧ (〈𝑉, 𝐸〉 Neighbors 𝐵) = {𝐴, 𝐶} ∧ (〈𝑉, 𝐸〉 Neighbors 𝐶) = {𝐴, 𝐵}))) |