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 are_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 are_collinear implies not a,b,d,o are_coplanar )
assume that
A1: not a,b,c,d are_coplanar and
A2: a,b,c,o are_coplanar and
A3: not a,b,o are_collinear ; :: thesis: not a,b,d,o are_coplanar
assume a,b,d,o are_coplanar ; :: thesis: contradiction
then A4: a,b,o,d are_coplanar by Th7;
a,b,o,c are_coplanar by A2, Th7;
hence contradiction by A1, A3, A4, Lm4; :: thesis: verum