Metamath Proof Explorer

Definition df-ifs

Description: The inner five segment configuration is an abbreviation for another congruence condition. See brifs and ifscgr for how it is used. Definition 4.1 of Schwabhauser p. 34. (Contributed by Scott Fenton, 26-Sep-2013)

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cifs ⊢ InnerFiveSeg
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 35 37 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 22 31 40 wbr ⊢ ⟨ 𝑐 , 𝑑 ⟩ Cgr ⟨ 𝑧 , 𝑤 ⟩
50 48 49 wa ⊢ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ Cgr ⟨ 𝑧 , 𝑤 ⟩ )
51 39 45 50 w3a ⊢ ( ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑐 ⟩ Cgr ⟨ 𝑥 , 𝑧 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ Cgr ⟨ 𝑧 , 𝑤 ⟩ ) )
52 24 33 51 w3a ⊢ ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑐 ⟩ Cgr ⟨ 𝑥 , 𝑧 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ Cgr ⟨ 𝑧 , 𝑤 ⟩ ) ) )
53 52 15 8 wrex ⊢ ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑐 ⟩ Cgr ⟨ 𝑥 , 𝑧 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ Cgr ⟨ 𝑧 , 𝑤 ⟩ ) ) )
54 53 14 8 wrex ⊢ ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑐 ⟩ Cgr ⟨ 𝑥 , 𝑧 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ Cgr ⟨ 𝑧 , 𝑤 ⟩ ) ) )
55 54 13 8 wrex ⊢ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑐 ⟩ Cgr ⟨ 𝑥 , 𝑧 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ Cgr ⟨ 𝑧 , 𝑤 ⟩ ) ) )
56 55 12 8 wrex ⊢ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑐 ⟩ Cgr ⟨ 𝑥 , 𝑧 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ Cgr ⟨ 𝑧 , 𝑤 ⟩ ) ) )
57 56 11 8 wrex ⊢ ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑐 ⟩ Cgr ⟨ 𝑥 , 𝑧 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ Cgr ⟨ 𝑧 , 𝑤 ⟩ ) ) )
58 57 10 8 wrex ⊢ ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑐 ⟩ Cgr ⟨ 𝑥 , 𝑧 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ Cgr ⟨ 𝑧 , 𝑤 ⟩ ) ) )
59 58 9 8 wrex ⊢ ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑐 ⟩ Cgr ⟨ 𝑥 , 𝑧 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ Cgr ⟨ 𝑧 , 𝑤 ⟩ ) ) )
60 59 5 8 wrex ⊢ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑐 ⟩ Cgr ⟨ 𝑥 , 𝑧 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ Cgr ⟨ 𝑧 , 𝑤 ⟩ ) ) )
61 60 3 4 wrex ⊢ ∃ 𝑛 ∈ ℕ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑐 ⟩ Cgr ⟨ 𝑥 , 𝑧 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ Cgr ⟨ 𝑧 , 𝑤 ⟩ ) ) )
62 61 1 2 copab ⊢ { ⟨ 𝑝 , 𝑞 ⟩ ∣ ∃ 𝑛 ∈ ℕ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑐 ⟩ Cgr ⟨ 𝑥 , 𝑧 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ Cgr ⟨ 𝑧 , 𝑤 ⟩ ) ) ) }
63 0 62 wceq ⊢ InnerFiveSeg = { ⟨ 𝑝 , 𝑞 ⟩ ∣ ∃ 𝑛 ∈ ℕ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑧 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑤 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , ⟨ 𝑐 , 𝑑 ⟩ ⟩ ∧ 𝑞 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , ⟨ 𝑧 , 𝑤 ⟩ ⟩ ∧ ( ( 𝑏 Btwn ⟨ 𝑎 , 𝑐 ⟩ ∧ 𝑦 Btwn ⟨ 𝑥 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑐 ⟩ Cgr ⟨ 𝑥 , 𝑧 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( ⟨ 𝑎 , 𝑑 ⟩ Cgr ⟨ 𝑥 , 𝑤 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ Cgr ⟨ 𝑧 , 𝑤 ⟩ ) ) ) }