∀e:EuclideanPlane. ∀A,B:Point. ∃C:Point. (AC=AB ∧ BC=AB ∧ AC=BC) supposing ¬(A = B ∈ Point)
{ Auto }
1. e : EuclideanPlane@i'
2. A : Point@i
3. B : Point@i
4. ¬(A = B ∈ Point)
⊢ ∃C:Point. (AC=AB ∧ BC=AB ∧ AC=BC)