---

Step * 2 1 1 1 of Lemma permutation-s-group-sep-or


1. rv : SeparationSpace
2. sepw : x:Point ⟶ y:{y:Point| x # y}  ⟶ x # y
3. ∀a,b:Point.  SqStable(a # b)
4. x1 : Point ⟶ Point
5. x2 : Point ⟶ Point
6. ∀x:Point. x1 (x2 x) ≡ x
7. ∀x:Point. x2 (x1 x) ≡ x
8. ∀x,y:Point.  (x1 x # x1 y ⇒ x # y)
9. ∀x,y:Point.  (x2 x # x2 y ⇒ x # y)
10. x3 : Point ⟶ Point
11. x4 : Point ⟶ Point
12. ∀x:Point. x3 (x4 x) ≡ x
13. ∀x:Point. x4 (x3 x) ≡ x
14. ∀x,y:Point.  (x3 x # x3 y ⇒ x # y)
15. ∀x,y:Point.  (x4 x # x4 y ⇒ x # y)
16. y1 : Point ⟶ Point
17. y2 : Point ⟶ Point
18. ∀x:Point. y1 (y2 x) ≡ x
19. ∀x:Point. y2 (y1 x) ≡ x
20. ∀x,y:Point.  (y1 x # y1 y ⇒ x # y)
21. ∀x,y:Point.  (y2 x # y2 y ⇒ x # y)
22. y3 : Point ⟶ Point
23. y4 : Point ⟶ Point
24. ∀x:Point. y3 (y4 x) ≡ x
25. ∀x:Point. y4 (y3 x) ≡ x
26. ∀x,y:Point.  (y3 x # y3 y ⇒ x # y)
27. ∀x,y:Point.  (y4 x # y4 y ⇒ x # y)
28. a : Point
29. y2 (x2 a) # y4 (x4 a)
30. y2 (x2 a) # y2 (x4 a)
⊢ x2 a # x4 a
BY
{ OnMaybeHyp 21 (\h. (BHyp h  THEN Try (Trivial) THEN MemCD THEN Trivial)) }

---

Latex:

---

Latex:

1.  rv  :  SeparationSpace
2.  sepw  :  x:Point  {}\mrightarrow{}  y:\{y:Point|  x  \#  y\}    {}\mrightarrow{}  x  \#  y
3.  \mforall{}a,b:Point.    SqStable(a  \#  b)
4.  x1  :  Point  {}\mrightarrow{}  Point
5.  x2  :  Point  {}\mrightarrow{}  Point
6.  \mforall{}x:Point.  x1  (x2  x)  \mequiv{}  x
7.  \mforall{}x:Point.  x2  (x1  x)  \mequiv{}  x
8.  \mforall{}x,y:Point.    (x1  x  \#  x1  y  {}\mRightarrow{}  x  \#  y)
9.  \mforall{}x,y:Point.    (x2  x  \#  x2  y  {}\mRightarrow{}  x  \#  y)
10.  x3  :  Point  {}\mrightarrow{}  Point
11.  x4  :  Point  {}\mrightarrow{}  Point
12.  \mforall{}x:Point.  x3  (x4  x)  \mequiv{}  x
13.  \mforall{}x:Point.  x4  (x3  x)  \mequiv{}  x
14.  \mforall{}x,y:Point.    (x3  x  \#  x3  y  {}\mRightarrow{}  x  \#  y)
15.  \mforall{}x,y:Point.    (x4  x  \#  x4  y  {}\mRightarrow{}  x  \#  y)
16.  y1  :  Point  {}\mrightarrow{}  Point
17.  y2  :  Point  {}\mrightarrow{}  Point
18.  \mforall{}x:Point.  y1  (y2  x)  \mequiv{}  x
19.  \mforall{}x:Point.  y2  (y1  x)  \mequiv{}  x
20.  \mforall{}x,y:Point.    (y1  x  \#  y1  y  {}\mRightarrow{}  x  \#  y)
21.  \mforall{}x,y:Point.    (y2  x  \#  y2  y  {}\mRightarrow{}  x  \#  y)
22.  y3  :  Point  {}\mrightarrow{}  Point
23.  y4  :  Point  {}\mrightarrow{}  Point
24.  \mforall{}x:Point.  y3  (y4  x)  \mequiv{}  x
25.  \mforall{}x:Point.  y4  (y3  x)  \mequiv{}  x
26.  \mforall{}x,y:Point.    (y3  x  \#  y3  y  {}\mRightarrow{}  x  \#  y)
27.  \mforall{}x,y:Point.    (y4  x  \#  y4  y  {}\mRightarrow{}  x  \#  y)
28.  a  :  Point
29.  y2  (x2  a)  \#  y4  (x4  a)
30.  y2  (x2  a)  \#  y2  (x4  a)
\mvdash{}  x2  a  \#  x4  a


By

---

Latex:
OnMaybeHyp  21  (\mbackslash{}h.  (BHyp  h    THEN  Try  (Trivial)  THEN  MemCD  THEN  Trivial))

---

Home Index