Metamath Proof Explorer

Definition df-ofs

Description: The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom ( ax5seg ). See brofs and 5segofs for how it is used. Definition 2.10 of Schwabhauser p. 28. (Contributed by Scott Fenton, 21-Sep-2013)

Ref Expression
Assertion df-ofs OuterFiveSeg = { ⟨ 𝑝 , 𝑞 ⟩ ∣ ∃ 𝑛 ∈ ℕ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩ ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cofs ⊢ OuterFiveSeg
1 vp ⊢ 𝑝
2 vq ⊢ 𝑞
3 vn ⊢ 𝑛
4 cn ⊢ ℕ
5 va ⊢ 𝑎
6 cee ⊢ 𝔼
7 3 cv ⊢ 𝑛
8 7 6 cfv ⊢ ( 𝔼 ‘ 𝑛 )
9 vb ⊢ 𝑏
10 vc ⊢ 𝑐
11 vd ⊢ 𝑑
12 vx ⊢ 𝑥
13 vy ⊢ 𝑦
14 vz ⊢ 𝑧
15 vw ⊢ 𝑤
16 1 cv ⊢ 𝑝
17 5 cv ⊢ 𝑎
18 9 cv ⊢ 𝑏
19 17 18 cop ⊢ ⟨ 𝑎 , 𝑏 ⟩
20 10 cv ⊢ 𝑐
21 11 cv ⊢ 𝑑
22 20 21 cop ⊢ ⟨ 𝑐 , 𝑑 ⟩
23 19 22 cop ⊢ ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩
24 16 23 wceq ⊢ 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩
25 2 cv ⊢ 𝑞
26 12 cv ⊢ 𝑥
27 13 cv ⊢ 𝑦
28 26 27 cop ⊢ ⟨ 𝑥 , 𝑦 ⟩
29 14 cv ⊢ 𝑧
30 15 cv ⊢ 𝑤
31 29 30 cop ⊢ ⟨ 𝑧 , 𝑤 ⟩
32 28 31 cop ⊢ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩
33 25 32 wceq ⊢ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩
34 cbtwn ⊢ Btwn
35 17 20 cop ⊢ ⟨ 𝑎 , 𝑐 ⟩
36 18 35 34 wbr ⊢ 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩
37 26 29 cop ⊢ ⟨ 𝑥 , 𝑧 ⟩
38 27 37 34 wbr ⊢ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩
39 36 38 wa ⊢ ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ )
40 ccgr ⊢ Cgr
41 19 28 40 wbr ⊢ ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑥 , 𝑦 ⟩
42 18 20 cop ⊢ ⟨ 𝑏 , 𝑐 ⟩
43 27 29 cop ⊢ ⟨ 𝑦 , 𝑧 ⟩
44 42 43 40 wbr ⊢ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑦 , 𝑧 ⟩
45 41 44 wa ⊢ ( ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑦 , 𝑧 ⟩ )
46 17 21 cop ⊢ ⟨ 𝑎 , 𝑑 ⟩
47 26 30 cop ⊢ ⟨ 𝑥 , 𝑤 ⟩
48 46 47 40 wbr ⊢ ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩
49 18 21 cop ⊢ ⟨ 𝑏 , 𝑑 ⟩
50 27 30 cop ⊢ ⟨ 𝑦 , 𝑤 ⟩
51 49 50 40 wbr ⊢ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩
52 48 51 wa ⊢ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩ )
53 39 45 52 w3a ⊢ ( ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩ ) )
54 24 33 53 w3a ⊢ ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩ ) ) )
55 54 15 8 wrex ⊢ ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩ ) ) )
56 55 14 8 wrex ⊢ ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩ ) ) )
57 56 13 8 wrex ⊢ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩ ) ) )
58 57 12 8 wrex ⊢ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩ ) ) )
59 58 11 8 wrex ⊢ ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩ ) ) )
60 59 10 8 wrex ⊢ ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩ ) ) )
61 60 9 8 wrex ⊢ ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩ ) ) )
62 61 5 8 wrex ⊢ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩ ) ) )
63 62 3 4 wrex ⊢ ∃ 𝑛 ∈ ℕ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩ ) ) )
64 63 1 2 copab ⊢ { ⟨ 𝑝 , 𝑞 ⟩ ∣ ∃ 𝑛 ∈ ℕ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩ ) ) ) }
65 0 64 wceq ⊢ OuterFiveSeg = { ⟨ 𝑝 , 𝑞 ⟩ ∣ ∃ 𝑛 ∈ ℕ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑏 , 𝑑 ⟩ Cgr ⟨ 𝑦 , 𝑤 ⟩ ) ) ) }