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 12 :: thesis:
assume that
A1: ( o <> q1 & p1 <> q1 & o <> q2 & p2 <> q2 & o <> q3 & p3 <> q3 ) and
A2: ( not o,p1,p2 is_collinear & not o,p1,p3 is_collinear & not o,p2,p3 is_collinear ) and
A3: ( p1,p2,r3 is_collinear & q1,q2,r3 is_collinear & p2,p3,r1 is_collinear & q2,q3,r1 is_collinear & p1,p3,r2 is_collinear & q1,q3,r2 is_collinear ) and
A4: ( o,p1,q1 is_collinear & o,p2,q2 is_collinear & o,p3,q3 is_collinear ) ; :: thesis:
consider o' being Element of V such that
A5: ( not o' is zero & o = Dir o' ) by ANPROJ_1:42;
consider p1', p2', r3' being Element of V such that
A6: ( p1 = Dir p1' & p2 = Dir p2' & r3 = Dir r3' & not p1' is zero & not p2' is zero & not r3' is zero & p1',p2',r3' are_LinDep ) by A3, Th24;
consider q1', q2', r3'' being Element of V such that
A7: ( q1 = Dir q1' & q2 = Dir q2' & r3 = Dir r3'' & not q1' is zero & not q2' is zero & not r3'' is zero & q1',q2',r3'' are_LinDep ) by A3, Th24;
A8: q1',q2',r3' are_LinDep

are_Prop r3'',r3' by A6, A7, ANPROJ_1:35;
hence q1',q2',r3' are_LinDep by A7, ANPROJ_1:9; :: thesis:

end;

consider p2'', p3', r1' being Element of V such that
A9: ( p2 = Dir p2'' & p3 = Dir p3' & r1 = Dir r1' & not p2'' is zero & not p3' is zero & not r1' is zero & p2'',p3',r1' are_LinDep ) by A3, Th24;
A10: p2',p3',r1' are_LinDep

are_Prop p2'',p2' by A6, A9, ANPROJ_1:35;
hence p2',p3',r1' are_LinDep by A9, ANPROJ_1:9; :: thesis:

end;

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

( are_Prop q2'',q2' & are_Prop r1'',r1' ) by A7, A9, A11, ANPROJ_1:35;
hence q2',q3',r1' are_LinDep by A11, ANPROJ_1:9; :: thesis:

end;

consider p1'', p3'', r2' being Element of V such that
A13: ( p1 = Dir p1'' & p3 = Dir p3'' & r2 = Dir r2' & not p1'' is zero & not p3'' is zero & not r2' is zero & p1'',p3'',r2' are_LinDep ) by A3, Th24;
A14: p1',p3',r2' are_LinDep

( are_Prop p1'',p1' & are_Prop p3'',p3' ) by A6, A9, A13, ANPROJ_1:35;
hence p1',p3',r2' are_LinDep by A13, ANPROJ_1:9; :: thesis:

end;

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

( are_Prop q1'',q1' & are_Prop q3'',q3' & are_Prop r2'',r2' ) by A7, A11, A13, A15, ANPROJ_1:35;
hence q1',q3',r2' are_LinDep by A15, ANPROJ_1:9; :: thesis:

end;

A17: ( not are_Prop o',q1' & not are_Prop o',q2' & not are_Prop o',q3' & not are_Prop p1',q1' & not are_Prop p2',q2' & not are_Prop p3',q3' ) by A1, A5, A6, A7, A9, A11, ANPROJ_1:35;
consider o'', p1''', q1''' being Element of V such that
A18: ( o = Dir o'' & p1 = Dir p1''' & q1 = Dir q1''' & not o'' is zero & not p1''' is zero & not q1''' is zero & o'',p1''',q1''' are_LinDep ) by A4, Th24;
A19: o',p1',q1' are_LinDep

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

end;

consider o''', p2''', q2''' being Element of V such that
A20: ( o = Dir o''' & p2 = Dir p2''' & q2 = Dir q2''' & not o''' is zero & not p2''' is zero & not q2''' is zero & o''',p2''',q2''' are_LinDep ) by A4, Th24;
A21: o',p2',q2' are_LinDep

( are_Prop o''',o' & are_Prop p2''',p2' & are_Prop q2''',q2' ) by A5, A6, A7, A20, ANPROJ_1:35;
hence o',p2',q2' are_LinDep by A20, ANPROJ_1:9; :: thesis:

end;

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

( are_Prop o'''',o' & are_Prop p3''',p3' & are_Prop q3''',q3' ) by A5, A9, A11, A22, ANPROJ_1:35;
hence o',p3',q3' are_LinDep by A22, ANPROJ_1:9; :: thesis:

end;

A24: p1',p2',p3' are_Prop_Vect by A6, A9, Def1;
A25: q1',q2',q3' are_Prop_Vect by A7, A11, Def1;
A26: r1',r2',r3' are_Prop_Vect by A6, A9, A13, Def1;
A27: o',p1',p2',p3',q1',q2',q3' are_perspective by A19, A21, A23, Def3;
A28: not o',p1',p2' are_LinDep by A2, A5, A6, Th24;
A29: not o',p1',p3' are_LinDep by A2, A5, A6, A9, Th24;
A30: not o',p2',p3' are_LinDep by A2, A5, A6, A9, Th24;
A31: p1',p2',p3',r1',r2',r3' lie_on_a_triangle by A6, A10, A14, Def2;
q1',q2',q3',r1',r2',r3' lie_on_a_triangle by A8, A12, A16, Def2;
then r1',r2',r3' are_LinDep by A5, A17, A24, A25, A26, A27, A28, A29, A30, A31, Th8;
hence r1,r2,r3 is_collinear by A6, A9, A13, Th24; :: thesis: