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