Metamath Proof Explorer

Theorem 3cyclfrgrrn1

Description: Every vertex in a friendship graph (with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 16-Nov-2017) (Revised by AV, 2-Apr-2021)

Ref Expression
Hypotheses 3cyclfrgrrn1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
3cyclfrgrrn1.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion 3cyclfrgrrn1 ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐶 ) → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 3cyclfrgrrn1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 3cyclfrgrrn1.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 1 2 2pthfrgrrn2 ⊢ ( 𝐺 ∈ FriendGraph → ∀ 𝑎 ∈ 𝑉 ∀ 𝑧 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃ 𝑥 ∈ 𝑉 ( ( { 𝑎 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧 ) ) )
4 necom ⊢ ( 𝐴 ≠ 𝐶 ↔ 𝐶 ≠ 𝐴 )
5 eldifsn ⊢ ( 𝐶 ∈ ( 𝑉 ∖ { 𝐴 } ) ↔ ( 𝐶 ∈ 𝑉 ∧ 𝐶 ≠ 𝐴 ) )
6 5 simplbi2com ⊢ ( 𝐶 ≠ 𝐴 → ( 𝐶 ∈ 𝑉 → 𝐶 ∈ ( 𝑉 ∖ { 𝐴 } ) ) )
7 4 6 sylbi ⊢ ( 𝐴 ≠ 𝐶 → ( 𝐶 ∈ 𝑉 → 𝐶 ∈ ( 𝑉 ∖ { 𝐴 } ) ) )
8 7 com12 ⊢ ( 𝐶 ∈ 𝑉 → ( 𝐴 ≠ 𝐶 → 𝐶 ∈ ( 𝑉 ∖ { 𝐴 } ) ) )
9 8 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐴 ≠ 𝐶 → 𝐶 ∈ ( 𝑉 ∖ { 𝐴 } ) ) )
10 9 imp ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐶 ) → 𝐶 ∈ ( 𝑉 ∖ { 𝐴 } ) )
11 sneq ⊢ ( 𝑎 = 𝐴 → { 𝑎 } = { 𝐴 } )
12 11 difeq2d ⊢ ( 𝑎 = 𝐴 → ( 𝑉 ∖ { 𝑎 } ) = ( 𝑉 ∖ { 𝐴 } ) )
13 preq1 ⊢ ( 𝑎 = 𝐴 → { 𝑎 , 𝑥 } = { 𝐴 , 𝑥 } )
14 13 eleq1d ⊢ ( 𝑎 = 𝐴 → ( { 𝑎 , 𝑥 } ∈ 𝐸 ↔ { 𝐴 , 𝑥 } ∈ 𝐸 ) )
15 14 anbi1d ⊢ ( 𝑎 = 𝐴 → ( ( { 𝑎 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) ↔ ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) ) )
16 neeq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 ≠ 𝑥 ↔ 𝐴 ≠ 𝑥 ) )
17 16 anbi1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧 ) ↔ ( 𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧 ) ) )
18 15 17 anbi12d ⊢ ( 𝑎 = 𝐴 → ( ( ( { 𝑎 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧 ) ) ↔ ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) ∧ ( 𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧 ) ) ) )
19 18 rexbidv ⊢ ( 𝑎 = 𝐴 → ( ∃ 𝑥 ∈ 𝑉 ( ( { 𝑎 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧 ) ) ↔ ∃ 𝑥 ∈ 𝑉 ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) ∧ ( 𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧 ) ) ) )
20 12 19 raleqbidv ⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑧 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃ 𝑥 ∈ 𝑉 ( ( { 𝑎 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧 ) ) ↔ ∀ 𝑧 ∈ ( 𝑉 ∖ { 𝐴 } ) ∃ 𝑥 ∈ 𝑉 ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) ∧ ( 𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧 ) ) ) )
21 20 rspcv ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑧 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃ 𝑥 ∈ 𝑉 ( ( { 𝑎 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧 ) ) → ∀ 𝑧 ∈ ( 𝑉 ∖ { 𝐴 } ) ∃ 𝑥 ∈ 𝑉 ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) ∧ ( 𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧 ) ) ) )
22 21 ad2antrr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐶 ) → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑧 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃ 𝑥 ∈ 𝑉 ( ( { 𝑎 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧 ) ) → ∀ 𝑧 ∈ ( 𝑉 ∖ { 𝐴 } ) ∃ 𝑥 ∈ 𝑉 ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) ∧ ( 𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧 ) ) ) )
23 preq2 ⊢ ( 𝑧 = 𝐶 → { 𝑥 , 𝑧 } = { 𝑥 , 𝐶 } )
24 23 eleq1d ⊢ ( 𝑧 = 𝐶 → ( { 𝑥 , 𝑧 } ∈ 𝐸 ↔ { 𝑥 , 𝐶 } ∈ 𝐸 ) )
25 24 anbi2d ⊢ ( 𝑧 = 𝐶 → ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) ↔ ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝐶 } ∈ 𝐸 ) ) )
26 neeq2 ⊢ ( 𝑧 = 𝐶 → ( 𝑥 ≠ 𝑧 ↔ 𝑥 ≠ 𝐶 ) )
27 26 anbi2d ⊢ ( 𝑧 = 𝐶 → ( ( 𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧 ) ↔ ( 𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶 ) ) )
28 25 27 anbi12d ⊢ ( 𝑧 = 𝐶 → ( ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) ∧ ( 𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧 ) ) ↔ ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝐶 } ∈ 𝐸 ) ∧ ( 𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶 ) ) ) )
29 28 rexbidv ⊢ ( 𝑧 = 𝐶 → ( ∃ 𝑥 ∈ 𝑉 ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) ∧ ( 𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧 ) ) ↔ ∃ 𝑥 ∈ 𝑉 ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝐶 } ∈ 𝐸 ) ∧ ( 𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶 ) ) ) )
30 29 rspcv ⊢ ( 𝐶 ∈ ( 𝑉 ∖ { 𝐴 } ) → ( ∀ 𝑧 ∈ ( 𝑉 ∖ { 𝐴 } ) ∃ 𝑥 ∈ 𝑉 ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) ∧ ( 𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧 ) ) → ∃ 𝑥 ∈ 𝑉 ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝐶 } ∈ 𝐸 ) ∧ ( 𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶 ) ) ) )
31 10 22 30 sylsyld ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐶 ) → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑧 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃ 𝑥 ∈ 𝑉 ( ( { 𝑎 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧 ) ) → ∃ 𝑥 ∈ 𝑉 ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝐶 } ∈ 𝐸 ) ∧ ( 𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶 ) ) ) )
32 1 2 2pthfrgrrn ⊢ ( 𝐺 ∈ FriendGraph → ∀ 𝑢 ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑢 } ) ∃ 𝑦 ∈ 𝑉 ( { 𝑢 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑣 } ∈ 𝐸 ) )
33 necom ⊢ ( 𝐴 ≠ 𝑥 ↔ 𝑥 ≠ 𝐴 )
34 eldifsn ⊢ ( 𝑥 ∈ ( 𝑉 ∖ { 𝐴 } ) ↔ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 𝐴 ) )
35 34 simplbi2com ⊢ ( 𝑥 ≠ 𝐴 → ( 𝑥 ∈ 𝑉 → 𝑥 ∈ ( 𝑉 ∖ { 𝐴 } ) ) )
36 33 35 sylbi ⊢ ( 𝐴 ≠ 𝑥 → ( 𝑥 ∈ 𝑉 → 𝑥 ∈ ( 𝑉 ∖ { 𝐴 } ) ) )
37 36 adantr ⊢ ( ( 𝐴 ≠ 𝑥 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑥 ∈ 𝑉 → 𝑥 ∈ ( 𝑉 ∖ { 𝐴 } ) ) )
38 37 imp ⊢ ( ( ( 𝐴 ≠ 𝑥 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) → 𝑥 ∈ ( 𝑉 ∖ { 𝐴 } ) )
39 sneq ⊢ ( 𝑢 = 𝐴 → { 𝑢 } = { 𝐴 } )
40 39 difeq2d ⊢ ( 𝑢 = 𝐴 → ( 𝑉 ∖ { 𝑢 } ) = ( 𝑉 ∖ { 𝐴 } ) )
41 preq1 ⊢ ( 𝑢 = 𝐴 → { 𝑢 , 𝑦 } = { 𝐴 , 𝑦 } )
42 41 eleq1d ⊢ ( 𝑢 = 𝐴 → ( { 𝑢 , 𝑦 } ∈ 𝐸 ↔ { 𝐴 , 𝑦 } ∈ 𝐸 ) )
43 42 anbi1d ⊢ ( 𝑢 = 𝐴 → ( ( { 𝑢 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑣 } ∈ 𝐸 ) ↔ ( { 𝐴 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑣 } ∈ 𝐸 ) ) )
44 43 rexbidv ⊢ ( 𝑢 = 𝐴 → ( ∃ 𝑦 ∈ 𝑉 ( { 𝑢 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑣 } ∈ 𝐸 ) ↔ ∃ 𝑦 ∈ 𝑉 ( { 𝐴 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑣 } ∈ 𝐸 ) ) )
45 40 44 raleqbidv ⊢ ( 𝑢 = 𝐴 → ( ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑢 } ) ∃ 𝑦 ∈ 𝑉 ( { 𝑢 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑣 } ∈ 𝐸 ) ↔ ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝐴 } ) ∃ 𝑦 ∈ 𝑉 ( { 𝐴 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑣 } ∈ 𝐸 ) ) )
46 45 rspcv ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑢 ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑢 } ) ∃ 𝑦 ∈ 𝑉 ( { 𝑢 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑣 } ∈ 𝐸 ) → ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝐴 } ) ∃ 𝑦 ∈ 𝑉 ( { 𝐴 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑣 } ∈ 𝐸 ) ) )
47 46 adantl ⊢ ( ( 𝐴 ≠ 𝑥 ∧ 𝐴 ∈ 𝑉 ) → ( ∀ 𝑢 ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑢 } ) ∃ 𝑦 ∈ 𝑉 ( { 𝑢 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑣 } ∈ 𝐸 ) → ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝐴 } ) ∃ 𝑦 ∈ 𝑉 ( { 𝐴 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑣 } ∈ 𝐸 ) ) )
48 47 adantr ⊢ ( ( ( 𝐴 ≠ 𝑥 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) → ( ∀ 𝑢 ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑢 } ) ∃ 𝑦 ∈ 𝑉 ( { 𝑢 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑣 } ∈ 𝐸 ) → ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝐴 } ) ∃ 𝑦 ∈ 𝑉 ( { 𝐴 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑣 } ∈ 𝐸 ) ) )
49 preq2 ⊢ ( 𝑣 = 𝑥 → { 𝑦 , 𝑣 } = { 𝑦 , 𝑥 } )
50 49 eleq1d ⊢ ( 𝑣 = 𝑥 → ( { 𝑦 , 𝑣 } ∈ 𝐸 ↔ { 𝑦 , 𝑥 } ∈ 𝐸 ) )
51 50 anbi2d ⊢ ( 𝑣 = 𝑥 → ( ( { 𝐴 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑣 } ∈ 𝐸 ) ↔ ( { 𝐴 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑥 } ∈ 𝐸 ) ) )
52 51 rexbidv ⊢ ( 𝑣 = 𝑥 → ( ∃ 𝑦 ∈ 𝑉 ( { 𝐴 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑣 } ∈ 𝐸 ) ↔ ∃ 𝑦 ∈ 𝑉 ( { 𝐴 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑥 } ∈ 𝐸 ) ) )
53 52 rspcv ⊢ ( 𝑥 ∈ ( 𝑉 ∖ { 𝐴 } ) → ( ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝐴 } ) ∃ 𝑦 ∈ 𝑉 ( { 𝐴 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑣 } ∈ 𝐸 ) → ∃ 𝑦 ∈ 𝑉 ( { 𝐴 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑥 } ∈ 𝐸 ) ) )
54 38 48 53 sylsyld ⊢ ( ( ( 𝐴 ≠ 𝑥 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) → ( ∀ 𝑢 ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑢 } ) ∃ 𝑦 ∈ 𝑉 ( { 𝑢 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑣 } ∈ 𝐸 ) → ∃ 𝑦 ∈ 𝑉 ( { 𝐴 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑥 } ∈ 𝐸 ) ) )
55 prcom ⊢ { 𝐴 , 𝑦 } = { 𝑦 , 𝐴 }
56 55 eleq1i ⊢ ( { 𝐴 , 𝑦 } ∈ 𝐸 ↔ { 𝑦 , 𝐴 } ∈ 𝐸 )
57 prcom ⊢ { 𝑦 , 𝑥 } = { 𝑥 , 𝑦 }
58 57 eleq1i ⊢ ( { 𝑦 , 𝑥 } ∈ 𝐸 ↔ { 𝑥 , 𝑦 } ∈ 𝐸 )
59 56 58 anbi12ci ⊢ ( ( { 𝐴 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑥 } ∈ 𝐸 ) ↔ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝐴 } ∈ 𝐸 ) )
60 preq2 ⊢ ( 𝑏 = 𝑥 → { 𝐴 , 𝑏 } = { 𝐴 , 𝑥 } )
61 60 eleq1d ⊢ ( 𝑏 = 𝑥 → ( { 𝐴 , 𝑏 } ∈ 𝐸 ↔ { 𝐴 , 𝑥 } ∈ 𝐸 ) )
62 preq1 ⊢ ( 𝑏 = 𝑥 → { 𝑏 , 𝑐 } = { 𝑥 , 𝑐 } )
63 62 eleq1d ⊢ ( 𝑏 = 𝑥 → ( { 𝑏 , 𝑐 } ∈ 𝐸 ↔ { 𝑥 , 𝑐 } ∈ 𝐸 ) )
64 biidd ⊢ ( 𝑏 = 𝑥 → ( { 𝑐 , 𝐴 } ∈ 𝐸 ↔ { 𝑐 , 𝐴 } ∈ 𝐸 ) )
65 61 63 64 3anbi123d ⊢ ( 𝑏 = 𝑥 → ( ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) ↔ ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) ) )
66 biidd ⊢ ( 𝑐 = 𝑦 → ( { 𝐴 , 𝑥 } ∈ 𝐸 ↔ { 𝐴 , 𝑥 } ∈ 𝐸 ) )
67 preq2 ⊢ ( 𝑐 = 𝑦 → { 𝑥 , 𝑐 } = { 𝑥 , 𝑦 } )
68 67 eleq1d ⊢ ( 𝑐 = 𝑦 → ( { 𝑥 , 𝑐 } ∈ 𝐸 ↔ { 𝑥 , 𝑦 } ∈ 𝐸 ) )
69 preq1 ⊢ ( 𝑐 = 𝑦 → { 𝑐 , 𝐴 } = { 𝑦 , 𝐴 } )
70 69 eleq1d ⊢ ( 𝑐 = 𝑦 → ( { 𝑐 , 𝐴 } ∈ 𝐸 ↔ { 𝑦 , 𝐴 } ∈ 𝐸 ) )
71 66 68 70 3anbi123d ⊢ ( 𝑐 = 𝑦 → ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) ↔ ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝐴 } ∈ 𝐸 ) ) )
72 65 71 rspc2ev ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝐴 } ∈ 𝐸 ) ) → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) )
73 72 3expa ⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ∧ ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝐴 } ∈ 𝐸 ) ) → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) )
74 73 expcom ⊢ ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝐴 } ∈ 𝐸 ) → ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) ) )
75 74 3expib ⊢ ( { 𝐴 , 𝑥 } ∈ 𝐸 → ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝐴 } ∈ 𝐸 ) → ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) ) ) )
76 59 75 syl5bi ⊢ ( { 𝐴 , 𝑥 } ∈ 𝐸 → ( ( { 𝐴 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑥 } ∈ 𝐸 ) → ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) ) ) )
77 76 adantr ⊢ ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝐶 } ∈ 𝐸 ) → ( ( { 𝐴 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑥 } ∈ 𝐸 ) → ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) ) ) )
78 77 com13 ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( ( { 𝐴 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑥 } ∈ 𝐸 ) → ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝐶 } ∈ 𝐸 ) → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) ) ) )
79 78 rexlimdva ⊢ ( 𝑥 ∈ 𝑉 → ( ∃ 𝑦 ∈ 𝑉 ( { 𝐴 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑥 } ∈ 𝐸 ) → ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝐶 } ∈ 𝐸 ) → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) ) ) )
80 79 com13 ⊢ ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝐶 } ∈ 𝐸 ) → ( ∃ 𝑦 ∈ 𝑉 ( { 𝐴 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑥 } ∈ 𝐸 ) → ( 𝑥 ∈ 𝑉 → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) ) ) )
81 54 80 syl9 ⊢ ( ( ( 𝐴 ≠ 𝑥 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) → ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝐶 } ∈ 𝐸 ) → ( ∀ 𝑢 ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑢 } ) ∃ 𝑦 ∈ 𝑉 ( { 𝑢 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑣 } ∈ 𝐸 ) → ( 𝑥 ∈ 𝑉 → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) ) ) ) )
82 81 exp31 ⊢ ( 𝐴 ≠ 𝑥 → ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ 𝑉 → ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝐶 } ∈ 𝐸 ) → ( ∀ 𝑢 ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑢 } ) ∃ 𝑦 ∈ 𝑉 ( { 𝑢 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑣 } ∈ 𝐸 ) → ( 𝑥 ∈ 𝑉 → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) ) ) ) ) ) )
83 82 com24 ⊢ ( 𝐴 ≠ 𝑥 → ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝐶 } ∈ 𝐸 ) → ( 𝑥 ∈ 𝑉 → ( 𝐴 ∈ 𝑉 → ( ∀ 𝑢 ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑢 } ) ∃ 𝑦 ∈ 𝑉 ( { 𝑢 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑣 } ∈ 𝐸 ) → ( 𝑥 ∈ 𝑉 → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) ) ) ) ) ) )
84 83 adantr ⊢ ( ( 𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶 ) → ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝐶 } ∈ 𝐸 ) → ( 𝑥 ∈ 𝑉 → ( 𝐴 ∈ 𝑉 → ( ∀ 𝑢 ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑢 } ) ∃ 𝑦 ∈ 𝑉 ( { 𝑢 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑣 } ∈ 𝐸 ) → ( 𝑥 ∈ 𝑉 → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) ) ) ) ) ) )
85 84 impcom ⊢ ( ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝐶 } ∈ 𝐸 ) ∧ ( 𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶 ) ) → ( 𝑥 ∈ 𝑉 → ( 𝐴 ∈ 𝑉 → ( ∀ 𝑢 ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑢 } ) ∃ 𝑦 ∈ 𝑉 ( { 𝑢 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑣 } ∈ 𝐸 ) → ( 𝑥 ∈ 𝑉 → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) ) ) ) ) )
86 85 com15 ⊢ ( 𝑥 ∈ 𝑉 → ( 𝑥 ∈ 𝑉 → ( 𝐴 ∈ 𝑉 → ( ∀ 𝑢 ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑢 } ) ∃ 𝑦 ∈ 𝑉 ( { 𝑢 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑣 } ∈ 𝐸 ) → ( ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝐶 } ∈ 𝐸 ) ∧ ( 𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶 ) ) → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) ) ) ) ) )
87 86 pm2.43i ⊢ ( 𝑥 ∈ 𝑉 → ( 𝐴 ∈ 𝑉 → ( ∀ 𝑢 ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑢 } ) ∃ 𝑦 ∈ 𝑉 ( { 𝑢 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑣 } ∈ 𝐸 ) → ( ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝐶 } ∈ 𝐸 ) ∧ ( 𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶 ) ) → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) ) ) ) )
88 87 com12 ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ 𝑉 → ( ∀ 𝑢 ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑢 } ) ∃ 𝑦 ∈ 𝑉 ( { 𝑢 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑣 } ∈ 𝐸 ) → ( ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝐶 } ∈ 𝐸 ) ∧ ( 𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶 ) ) → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) ) ) ) )
89 88 ad2antrr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐶 ) → ( 𝑥 ∈ 𝑉 → ( ∀ 𝑢 ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑢 } ) ∃ 𝑦 ∈ 𝑉 ( { 𝑢 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑣 } ∈ 𝐸 ) → ( ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝐶 } ∈ 𝐸 ) ∧ ( 𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶 ) ) → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) ) ) ) )
90 89 com4t ⊢ ( ∀ 𝑢 ∈ 𝑉 ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑢 } ) ∃ 𝑦 ∈ 𝑉 ( { 𝑢 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑣 } ∈ 𝐸 ) → ( ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝐶 } ∈ 𝐸 ) ∧ ( 𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶 ) ) → ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐶 ) → ( 𝑥 ∈ 𝑉 → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) ) ) ) )
91 32 90 syl ⊢ ( 𝐺 ∈ FriendGraph → ( ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝐶 } ∈ 𝐸 ) ∧ ( 𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶 ) ) → ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐶 ) → ( 𝑥 ∈ 𝑉 → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) ) ) ) )
92 91 com14 ⊢ ( 𝑥 ∈ 𝑉 → ( ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝐶 } ∈ 𝐸 ) ∧ ( 𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶 ) ) → ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐶 ) → ( 𝐺 ∈ FriendGraph → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) ) ) ) )
93 92 rexlimiv ⊢ ( ∃ 𝑥 ∈ 𝑉 ( ( { 𝐴 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝐶 } ∈ 𝐸 ) ∧ ( 𝐴 ≠ 𝑥 ∧ 𝑥 ≠ 𝐶 ) ) → ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐶 ) → ( 𝐺 ∈ FriendGraph → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) ) ) )
94 31 93 syl6 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐶 ) → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑧 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃ 𝑥 ∈ 𝑉 ( ( { 𝑎 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧 ) ) → ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐶 ) → ( 𝐺 ∈ FriendGraph → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) ) ) ) )
95 94 pm2.43a ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐶 ) → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑧 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃ 𝑥 ∈ 𝑉 ( ( { 𝑎 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧 ) ) → ( 𝐺 ∈ FriendGraph → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) ) ) )
96 95 ex ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐴 ≠ 𝐶 → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑧 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃ 𝑥 ∈ 𝑉 ( ( { 𝑎 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧 ) ) → ( 𝐺 ∈ FriendGraph → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) ) ) ) )
97 96 com4t ⊢ ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑧 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃ 𝑥 ∈ 𝑉 ( ( { 𝑎 , 𝑥 } ∈ 𝐸 ∧ { 𝑥 , 𝑧 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑥 ∧ 𝑥 ≠ 𝑧 ) ) → ( 𝐺 ∈ FriendGraph → ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐴 ≠ 𝐶 → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) ) ) ) )
98 3 97 mpcom ⊢ ( 𝐺 ∈ FriendGraph → ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐴 ≠ 𝐶 → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) ) ) )
99 98 3imp ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ 𝐴 ≠ 𝐶 ) → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝐴 } ∈ 𝐸 ) )