let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for a, a9, b, b9, c, c9, o being Element of FCPS st not a,b,c,o are_coplanar & o,a,a9 are_collinear & o,b,b9 are_collinear & o,c,c9 are_collinear & o <> a9 & o <> b9 & o <> c9 holds
( not a9,b9,c9 are_collinear & not a9,b9,c9,o are_coplanar )
let a, a9, b, b9, c, c9, o be Element of FCPS; :: thesis: ( not a,b,c,o are_coplanar & o,a,a9 are_collinear & o,b,b9 are_collinear & o,c,c9 are_collinear & o <> a9 & o <> b9 & o <> c9 implies ( not a9,b9,c9 are_collinear & not a9,b9,c9,o are_coplanar ) )
assume that
A1: ( not a,b,c,o are_coplanar & o,a,a9 are_collinear ) and
A2: o,b,b9 are_collinear and
A3: o,c,c9 are_collinear and
A4: o <> a9 and
A5: o <> b9 and
A6: o <> c9 ; :: thesis: ( not a9,b9,c9 are_collinear & not a9,b9,c9,o are_coplanar )
( a,o,a9 are_collinear & not o,b,c,a are_coplanar ) by A1, Th1, Th7;
then not o,b,c,a9 are_coplanar by A4, Th15;
then A7: not o,a9,b,c are_coplanar by Th7;
c,o,c9 are_collinear by A3, Th1;
then not o,a9,b,c9 are_coplanar by A6, A7, Th15;
then A8: not o,a9,c9,b are_coplanar by Th7;
b,o,b9 are_collinear by A2, Th1;
then not o,a9,c9,b9 are_coplanar by A5, A8, Th15;
then not a9,b9,c9,o are_coplanar by Th7;
hence ( not a9,b9,c9 are_collinear & not a9,b9,c9,o are_coplanar ) by Th6; :: thesis: verum