let OAS be OAffinSpace; :: thesis: OAS is Fanoian
let a be Element of OAS; :: according to PASCH:def 6 :: thesis: for b, c, d being Element of OAS st a,b // c,d & a,c // b,d & not LIN a,b,c holds
ex x being Element of OAS st
( Mid a,x,d & Mid b,x,c )
let b, c, d be Element of OAS; :: thesis: ( a,b // c,d & a,c // b,d & not LIN a,b,c implies ex x being Element of OAS st
( Mid a,x,d & Mid b,x,c ) )
assume that
A1: a,b // c,d and
a,c // b,d and
A2: not LIN a,b,c ; :: thesis: ex x being Element of OAS st
( Mid a,x,d & Mid b,x,c )
thus ex x being Element of OAS st
( Mid a,x,d & Mid b,x,c ) by A1, A2, Th30; :: thesis: verum