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 A1: ( not a,b,c,o are_coplanar & o,a,a' is_collinear & a <> a' ) ; :: thesis: not a,b,c,a' are_coplanar
assume A2: a,b,c,a' are_coplanar ; :: thesis: contradiction
( a,a',o is_collinear & a,b,c,a are_coplanar ) by A1, Th1, Th18;
hence contradiction by A1, A2, Th14; :: thesis: verum