let AFP be AffinPlane; :: thesis: 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 )
let a, b, c, d be Element of AFP; :: thesis: ( AFP is Fanoian & a,b // c,d & a,c // b,d & not LIN a,b,c implies ex p being Element of AFP st
( LIN b,c,p & LIN a,d,p ) )
assume ( ( for a, b, c, d being Element of AFP st a,b // c,d & a,c // b,d & a,d // b,c holds
LIN a,b,c ) & a,b // c,d & a,c // b,d & not LIN a,b,c ) ; :: according to TRANSLAC:def 1 :: thesis: ex p being Element of AFP st
( LIN b,c,p & LIN a,d,p )
then not a,d // b,c ;
then ex p being Element of AFP st
( LIN a,d,p & LIN b,c,p ) by AFF_1:60;
hence ex p being Element of AFP st
( LIN b,c,p & LIN a,d,p ) ; :: thesis: verum