let OAS be OAffinSpace; :: thesis: for a, b, c, d, p being Element of OAS st a,b '||' c,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 & not LIN a,b,c & LIN p,a,d & LIN p,b,c implies not LIN p,a,b )
assume that
A1: a,b '||' c,d and
A2: not LIN a,b,c and
A3: LIN p,a,d and
A4: LIN p,b,c ; :: thesis: not LIN p,a,b
A5: LIN p,a,a by DIRAF:31;
assume LIN p,a,b ; :: thesis: contradiction
then A6: LIN a,b,d by A2, A3, A4, A5, DIRAF:32;
A7: a,b '||' d,c by A1, DIRAF:22;
a <> b by A2, DIRAF:31;
hence contradiction by A2, A6, A7, DIRAF:33; :: thesis: verum