let FCPS be up-3-dimensional CollProjectiveSpace; :: thesis: for a, b, c, o, a', b', c' being Element of FCPS st not a,b,c,o are_coplanar & o,a,a' is_collinear & o,b,b' is_collinear & o,c,c' is_collinear & o <> a' & o <> b' & o <> c' holds
( not a',b',c' is_collinear & not a',b',c',o are_coplanar )
let a, b, c, o, a', b', c' be Element of FCPS; :: thesis: ( not a,b,c,o are_coplanar & o,a,a' is_collinear & o,b,b' is_collinear & o,c,c' is_collinear & o <> a' & o <> b' & o <> c' implies ( not a',b',c' is_collinear & not a',b',c',o are_coplanar ) )
assume A1: ( not a,b,c,o are_coplanar & o,a,a' is_collinear & o,b,b' is_collinear & o,c,c' is_collinear & o <> a' & o <> b' & o <> c' ) ; :: thesis: ( not a',b',c' is_collinear & not a',b',c',o are_coplanar )
then ( a,o,a' is_collinear & not o,b,c,a are_coplanar ) by Th1, Th11;
then not o,b,c,a' are_coplanar by A1, Th19;
then ( not o,a',b,c are_coplanar & c,o,c' is_collinear ) by A1, Th1, Th11;
then not o,a',b,c' are_coplanar by A1, Th19;
then ( not o,a',c',b are_coplanar & b,o,b' is_collinear ) by A1, Th1, Th11;
then not o,a',c',b' are_coplanar by A1, Th19;
then not a',b',c',o are_coplanar by Th11;
hence ( not a',b',c' is_collinear & not a',b',c',o are_coplanar ) by Th10; :: thesis: verum