let o, p1, p2, p3, q1, q2, q3, r1, r2, r3 be Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis:
assume that
A1: ( o <> p2 & o <> p3 & p2 <> p3 & p1 <> p2 & p1 <> p3 & o <> q2 & o <> q3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not o,p1,q1 are_collinear & o,p1,p2 are_collinear & o,p1,p3 are_collinear & o,q1,q2 are_collinear & o,q1,q3 are_collinear & p1,q2,r3 are_collinear & q1,p2,r3 are_collinear & p1,q3,r2 are_collinear & p3,q1,r2 are_collinear & p2,q3,r1 are_collinear & p3,q2,r1 are_collinear ) and
A2: not p1,q1,r1 are_collinear ; :: thesis:
consider pp1 being Element of (TOP-REAL 3) such that
A3: ( not pp1 is zero & Dir pp1 = p1 ) by ANPROJ_1:26;
consider pp2 being Element of (TOP-REAL 3) such that
A4: ( not pp2 is zero & Dir pp2 = p2 ) by ANPROJ_1:26;
consider pp3 being Element of (TOP-REAL 3) such that
A5: ( not pp3 is zero & Dir pp3 = p3 ) by ANPROJ_1:26;
consider pp4 being Element of (TOP-REAL 3) such that
A6: ( not pp4 is zero & Dir pp4 = q1 ) by ANPROJ_1:26;
consider pp5 being Element of (TOP-REAL 3) such that
A7: ( not pp5 is zero & Dir pp5 = q2 ) by ANPROJ_1:26;
consider pp6 being Element of (TOP-REAL 3) such that
A8: ( not pp6 is zero & Dir pp6 = q3 ) by ANPROJ_1:26;
consider pp7 being Element of (TOP-REAL 3) such that
A9: ( not pp7 is zero & Dir pp7 = r1 ) by ANPROJ_1:26;
consider pp8 being Element of (TOP-REAL 3) such that
A10: ( not pp8 is zero & Dir pp8 = r2 ) by ANPROJ_1:26;
consider pp9 being Element of (TOP-REAL 3) such that
A11: ( not pp9 is zero & Dir pp9 = r3 ) by ANPROJ_1:26;
not r1,p1,q1 are_collinear by A2, ANPROJ_2:24;
then A12: |{pp7,pp1,pp4}| <> 0 by A3, A6, A9, BKMODEL1:1;
|{pp7,pp1,pp4}| * |{pp7,pp8,pp9}| = 0

end;

then reconsider r142 = |{pp1,pp4,pp2}|, r173 = |{pp1,pp7,pp3}|, r143 = |{pp1,pp4,pp3}|, r172 = |{pp1,pp7,pp2}|, r145 = |{pp1,pp4,pp5}|, r179 = |{pp1,pp7,pp9}|, r149 = |{pp1,pp4,pp9}|, r175 = |{pp1,pp7,pp5}|, r148 = |{pp1,pp4,pp8}|, r176 = |{pp1,pp7,pp6}|, r146 = |{pp1,pp4,pp6}|, r178 = |{pp1,pp7,pp8}|, r475 = |{pp4,pp7,pp5}|, r416 = |{pp4,pp1,pp6}|, r476 = |{pp4,pp7,pp6}|, r415 = |{pp4,pp1,pp5}|, r478 = |{pp4,pp7,pp8}|, r413 = |{pp4,pp1,pp3}|, r473 = |{pp4,pp7,pp3}|, r418 = |{pp4,pp1,pp8}|, r472 = |{pp4,pp7,pp2}|, r419 = |{pp4,pp1,pp9}|, r479 = |{pp4,pp7,pp9}|, r412 = |{pp4,pp1,pp2}|, r712 = |{pp7,pp1,pp2}|, r746 = |{pp7,pp4,pp6}|, r716 = |{pp7,pp1,pp6}|, r742 = |{pp7,pp4,pp2}|, r715 = |{pp7,pp1,pp5}|, r743 = |{pp7,pp4,pp3}|, r713 = |{pp7,pp1,pp3}|, r745 = |{pp7,pp4,pp5}|, r749 = |{pp7,pp4,pp9}|, r718 = |{pp7,pp1,pp8}|, r719 = |{pp7,pp1,pp9}|, r748 = |{pp7,pp4,pp8}| as non zero Real by A3, A4, A5, A6, A7, A8, A9, A10, A11, BKMODEL1:1;
A13: r718 * r749 = r719 * r748

proof

A14: ( r142 * r173 = r143 * r172 & r145 * r179 = r149 * r175 & r148 * r176 = r146 * r178 & r475 * r416 = r476 * r415 & r478 * r413 = r473 * r418 & r472 * r419 = r479 * r412 & r712 * r746 = r716 * r742 & r715 * r743 = r713 * r745 )

proof

A15: ( p1,p2,p3 are_collinear & p1,q2,r3 are_collinear & p1,r2,q3 are_collinear & q1,q2,q3 are_collinear ) by A1, Th6;
( q1,r2,p3 are_collinear & q1,p2,r3 are_collinear & r1,p2,q3 are_collinear & r1,q2,p3 are_collinear ) by A1, Th6;
hence ( r142 * r173 = r143 * r172 & r145 * r179 = r149 * r175 & r148 * r176 = r146 * r178 & r475 * r416 = r476 * r415 & r478 * r413 = r473 * r418 & r472 * r419 = r479 * r412 & r712 * r746 = r716 * r742 & r715 * r743 = r713 * r745 ) by A15, A3, A4, A11, A8, A10, A6, A5, A7, A9, Th2; :: thesis:

end;

( r146 = - r416 & r145 = - r415 & r143 = - r413 & r148 = - r418 & r149 = - r419 & r142 = - r412 & r172 = - r712 & r476 = - r746 & r176 = - r716 & r472 = - r742 & r175 = - r715 & r473 = - r743 & r173 = - r713 & r475 = - r745 & r478 = - r748 & r479 = - r749 & r178 = - r718 & r179 = - r719 ) by ANPROJ_8:30;
hence r718 * r749 = r719 * r748 by A14, Th3; :: thesis:

end;

((|{pp7,pp1,pp4}| * |{pp7,pp8,pp9}|) - (|{pp7,pp1,pp8}| * |{pp7,pp4,pp9}|)) + (|{pp7,pp1,pp9}| * |{pp7,pp4,pp8}|) = 0 by ANPROJ_8:28;
hence |{pp7,pp1,pp4}| * |{pp7,pp8,pp9}| = 0 by A13; :: thesis:

end;

then |{pp7,pp8,pp9}| = 0 by A12, XCMPLX_1:6;
hence r1,r2,r3 are_collinear by A9, A10, A11, BKMODEL1:1; :: thesis: