let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for a, b, c, o, a9 being Element of FCPS st not a,b,c,o are_coplanar & o,a,a9 is_collinear & a <> a9 holds
not a,b,c,a9 are_coplanar
let a, b, c, o, a9 be Element of FCPS; :: thesis: ( not a,b,c,o are_coplanar & o,a,a9 is_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 is_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 Th18;
a,a9,o is_collinear by A2, Th1;
hence contradiction by A1, A3, A4, A5, Th14; :: thesis: verum