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