∀[e:EuclideanPlane]. ∀[x:Point]. ∀[m:Line].  ¬x # m supposing x I m
{ Auto }
1. e : EuclideanPlane
2. x : Point
3. m : Line
4. x I m
⊢ ¬x # m