let V be up-3-dimensional RealLinearSpace; :: thesis:
let o, p1, p2, p3, q1, q2, q3, r1, r2, r3 be Element of (ProjectiveSpace V); :: according to ANPROJ_2:def 13 :: thesis:
assume that
A1: ( o <> p2 & o <> p3 & p2 <> p3 & p1 <> p2 & p1 <> p3 & o <> q2 & o <> q3 & q2 <> q3 & q1 <> q2 & q1 <> q3 ) and
A2: not o,p1,q1 is_collinear and
A3: ( o,p1,p2 is_collinear & o,p1,p3 is_collinear & o,q1,q2 is_collinear & o,q1,q3 is_collinear ) and
A4: ( p1,q2,r3 is_collinear & q1,p2,r3 is_collinear & p1,q3,r2 is_collinear & p3,q1,r2 is_collinear & p2,q3,r1 is_collinear & p3,q2,r1 is_collinear ) ; :: thesis:
consider o', p1', p2' being Element of V such that
A5: ( o = Dir o' & p1 = Dir p1' & p2 = Dir p2' & not o' is zero & not p1' is zero & not p2' is zero & o',p1',p2' are_LinDep ) by A3, Th24;
consider o'', p1'', p3' being Element of V such that
A6: ( o = Dir o'' & p1 = Dir p1'' & p3 = Dir p3' & not o'' is zero & not p1'' is zero & not p3' is zero & o'',p1'',p3' are_LinDep ) by A3, Th24;
A7: o',p1',p3' are_LinDep

( are_Prop o'',o' & are_Prop p1'',p1' ) by A5, A6, ANPROJ_1:35;
hence o',p1',p3' are_LinDep by A6, ANPROJ_1:9; :: thesis:

end;

consider o''', q1', q2' being Element of V such that
A8: ( o = Dir o''' & q1 = Dir q1' & q2 = Dir q2' & not o''' is zero & not q1' is zero & not q2' is zero & o''',q1',q2' are_LinDep ) by A3, Th24;
A9: o',q1',q2' are_LinDep

are_Prop o''',o' by A5, A8, ANPROJ_1:35;
hence o',q1',q2' are_LinDep by A8, ANPROJ_1:9; :: thesis:

end;

consider o'''', q1'', q3' being Element of V such that
A10: ( o = Dir o'''' & q1 = Dir q1'' & q3 = Dir q3' & not o'''' is zero & not q1'' is zero & not q3' is zero & o'''',q1'',q3' are_LinDep ) by A3, Th24;
A11: o',q1',q3' are_LinDep

( are_Prop o'''',o' & are_Prop q1'',q1' ) by A5, A8, A10, ANPROJ_1:35;
hence o',q1',q3' are_LinDep by A10, ANPROJ_1:9; :: thesis:

end;

not o',p1',q1' are_LinDep by A2, A5, A8, Th24;
then A12: o',p1',p2',p3',q1',q2',q3' lie_on_an_angle by A5, A7, A9, A11, Def4;
( not are_Prop o',p2' & not are_Prop o',p3' & not are_Prop o',q2' & not are_Prop o',q3' & not are_Prop p1',p2' & not are_Prop p1',p3' & not are_Prop q1',q2' & not are_Prop q1',q3' & not are_Prop p2',p3' & not are_Prop q2',q3' ) by A1, A5, A6, A8, A10, ANPROJ_1:35;
then A13: o',p1',p2',p3',q1',q2',q3' are_half_mutually_not_Prop by Def5;
A14: ( p1',p2',p3' are_Prop_Vect & q1',q2',q3' are_Prop_Vect ) by A5, A6, A8, A10, Def1;
consider p1''', q2''', r3' being Element of V such that
A15: ( p1 = Dir p1''' & q2 = Dir q2''' & r3 = Dir r3' & not p1''' is zero & not q2''' is zero & not r3' is zero & p1''',q2''',r3' are_LinDep ) by A4, Th24;
A16: p1',q2',r3' are_LinDep

( are_Prop p1''',p1' & are_Prop q2''',q2' ) by A5, A8, A15, ANPROJ_1:35;
hence p1',q2',r3' are_LinDep by A15, ANPROJ_1:9; :: thesis:

end;

consider q1''', p2''', r3'' being Element of V such that
A17: ( q1 = Dir q1''' & p2 = Dir p2''' & r3 = Dir r3'' & not q1''' is zero & not p2''' is zero & not r3'' is zero & q1''',p2''',r3'' are_LinDep ) by A4, Th24;
A18: q1',p2',r3' are_LinDep

( are_Prop q1''',q1' & are_Prop p2''',p2' & are_Prop r3'',r3' ) by A5, A8, A15, A17, ANPROJ_1:35;
hence q1',p2',r3' are_LinDep by A17, ANPROJ_1:9; :: thesis:

end;

consider p1'''', q3'', r2' being Element of V such that
A19: ( p1 = Dir p1'''' & q3 = Dir q3'' & r2 = Dir r2' & not p1'''' is zero & not q3'' is zero & not r2' is zero & p1'''',q3'',r2' are_LinDep ) by A4, Th24;
A20: p1',q3',r2' are_LinDep

( are_Prop p1'''',p1' & are_Prop q3'',q3' ) by A5, A10, A19, ANPROJ_1:35;
hence p1',q3',r2' are_LinDep by A19, ANPROJ_1:9; :: thesis:

end;

consider p3'', q1''', r2'' being Element of V such that
A21: ( p3 = Dir p3'' & q1 = Dir q1''' & r2 = Dir r2'' & not p3'' is zero & not q1''' is zero & not r2'' is zero & p3'',q1''',r2'' are_LinDep ) by A4, Th24;
A22: p3',q1',r2' are_LinDep

( are_Prop p3'',p3' & are_Prop q1''',q1' & are_Prop r2'',r2' ) by A6, A8, A19, A21, ANPROJ_1:35;
hence p3',q1',r2' are_LinDep by A21, ANPROJ_1:9; :: thesis:

end;

consider p2'''', q3''', r1' being Element of V such that
A23: ( p2 = Dir p2'''' & q3 = Dir q3''' & r1 = Dir r1' & not p2'''' is zero & not q3''' is zero & not r1' is zero & p2'''',q3''',r1' are_LinDep ) by A4, Th24;
A24: p2',q3',r1' are_LinDep

( are_Prop p2'''',p2' & are_Prop q3''',q3' ) by A5, A10, A23, ANPROJ_1:35;
hence p2',q3',r1' are_LinDep by A23, ANPROJ_1:9; :: thesis:

end;

consider p3''', q2'''', r1'' being Element of V such that
A25: ( p3 = Dir p3''' & q2 = Dir q2'''' & r1 = Dir r1'' & not p3''' is zero & not q2'''' is zero & not r1'' is zero & p3''',q2'''',r1'' are_LinDep ) by A4, Th24;
A26: p3',q2',r1' are_LinDep

( are_Prop p3''',p3' & are_Prop q2'''',q2' & are_Prop r1'',r1' ) by A6, A8, A23, A25, ANPROJ_1:35;
hence p3',q2',r1' are_LinDep by A25, ANPROJ_1:9; :: thesis:

end;

r1',r2',r3' are_Prop_Vect by A15, A19, A23, Def1;
then r1',r2',r3' are_LinDep by A5, A12, A13, A14, A16, A18, A20, A22, A24, A26, Th9;
hence r1,r2,r3 is_collinear by A15, A19, A23, Th24; :: thesis: