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