∀e:BasicGeometry. ∀a,b,p,q:Point.  (a-pq-b 
⇒ b-pq-a)
{ Auto }
1. e : BasicGeometry
2. a : Point
3. b : Point
4. p : Point
5. q : Point
6. a-pq-b
⊢ b-pq-a