let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for a, b, c, d, o being Element of FCPS st not a,b,c,d are_coplanar & a,b,c,o are_coplanar & not a,b,o is_collinear holds
not a,b,d,o are_coplanar
let a, b, c, d, o be Element of FCPS; :: thesis: ( not a,b,c,d are_coplanar & a,b,c,o are_coplanar & not a,b,o is_collinear implies not a,b,d,o are_coplanar )
assume A1: ( not a,b,c,d are_coplanar & a,b,c,o are_coplanar & not a,b,o is_collinear ) ; :: thesis: not a,b,d,o are_coplanar
assume a,b,d,o are_coplanar ; :: thesis: contradiction
then A2: a,b,o,d are_coplanar by Th11;
a,b,o,c are_coplanar by A1, Th11;
hence contradiction by A1, A2, Lm4; :: thesis: verum