let FCPS be up-3-dimensional CollProjectiveSpace; 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; ( 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
; not a,b,d,o are_coplanar
assume
a,b,d,o are_coplanar
; 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; verum