let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for a, a9, b, c, o being Element of FCPS st not a,b,c,o are_coplanar & o,a,a9 are_collinear & a <> a9 holds
not a,b,c,a9 are_coplanar
let a, a9, b, c, o be Element of FCPS; :: thesis: ( not a,b,c,o are_coplanar & o,a,a9 are_collinear & a <> a9 implies not a,b,c,a9 are_coplanar )
assume that
A1: not a,b,c,o are_coplanar and
A2: o,a,a9 are_collinear and
A3: a <> a9 ; :: thesis: not a,b,c,a9 are_coplanar
assume A4: a,b,c,a9 are_coplanar ; :: thesis: contradiction
A5: a,b,c,a are_coplanar by Th14;
a,a9,o are_collinear by A2, Th1;
hence contradiction by A1, A3, A4, A5, Th10; :: thesis: verum