let OAS be OAffinSpace; :: thesis: for a, b, c, d, p being Element of OAS st a,b '||' c,d & a,c '||' b,d & not LIN a,b,c & LIN p,a,d & LIN p,b,c holds
not LIN p,a,b
let a, b, c, d, p be Element of OAS; :: thesis: ( a,b '||' c,d & a,c '||' b,d & not LIN a,b,c & LIN p,a,d & LIN p,b,c implies not LIN p,a,b )
assume A1: ( a,b '||' c,d & a,c '||' b,d & not LIN a,b,c & LIN p,a,d & LIN p,b,c ) ; :: thesis: not LIN p,a,b
assume A2: LIN p,a,b ; :: thesis: contradiction
( p <> a & LIN p,a,a ) by A1, DIRAF:37;
then ( a <> b & LIN a,b,d & a,b '||' d,c ) by A1, A2, DIRAF:27, DIRAF:38;
hence contradiction by A1, DIRAF:39; :: thesis: verum