for AFP being AffinPlane
for a, b, c, d being Element of AFP st AFP is Fanoian & a,b // c,d & a,c // b,d & not LIN a,b,c holds
ex p being Element of AFP st
( LIN b,c,p & LIN a,d,p )