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