let V be non trivial RealLinearSpace; :: thesis:
let p1, r2, q, r1, q1, p, r be Element of (ProjectiveSpace V); :: thesis:
assume A1: ( p1,r2,q is_collinear & r1,q1,q is_collinear & p1,r1,p is_collinear & r2,q1,p is_collinear & p1,q1,r is_collinear & r2,r1,r is_collinear & p,q,r is_collinear ) ; :: thesis:
then consider u, v, z being Element of V such that
A2: ( p1 = Dir u & r2 = Dir v & q = Dir z & not u is zero & not v is zero & not z is zero & u,v,z are_LinDep ) by Th24;
consider w, y, z1 being Element of V such that
A3: ( r1 = Dir w & q1 = Dir y & q = Dir z1 & not w is zero & not y is zero & not z1 is zero & w,y,z1 are_LinDep ) by A1, Th24;
consider u1, w1, x being Element of V such that
A4: ( p1 = Dir u1 & r1 = Dir w1 & p = Dir x & not u1 is zero & not w1 is zero & not x is zero & u1,w1,x are_LinDep ) by A1, Th24;
consider v1, y1, x1 being Element of V such that
A5: ( r2 = Dir v1 & q1 = Dir y1 & p = Dir x1 & not v1 is zero & not y1 is zero & not x1 is zero & v1,y1,x1 are_LinDep ) by A1, Th24;
consider u2, y2, t being Element of V such that
A6: ( p1 = Dir u2 & q1 = Dir y2 & r = Dir t & not u2 is zero & not y2 is zero & not t is zero & u2,y2,t are_LinDep ) by A1, Th24;
consider v2, w2, t1 being Element of V such that
A7: ( r2 = Dir v2 & r1 = Dir w2 & r = Dir t1 & not v2 is zero & not w2 is zero & not t1 is zero & v2,w2,t1 are_LinDep ) by A1, Th24;
consider x2, z2, t2 being Element of V such that
A8: ( p = Dir x2 & q = Dir z2 & r = Dir t2 & not x2 is zero & not z2 is zero & not t2 is zero & x2,z2,t2 are_LinDep ) by A1, Th24;
( u,v,z are_LinDep & w,y,z are_LinDep & u,w,x are_LinDep & v,y,x are_LinDep & u,y,t are_LinDep & v,w,t are_LinDep & x,z,t are_LinDep )

proof

A9: ( are_Prop z1,z & are_Prop w1,w & are_Prop u1,u ) by A2, A3, A4, ANPROJ_1:35;
A10: ( are_Prop y1,y & are_Prop x1,x ) by A3, A4, A5, ANPROJ_1:35;
A11: ( are_Prop u2,u & are_Prop y2,y ) by A2, A3, A6, ANPROJ_1:35;
A12: ( are_Prop v2,v & are_Prop w2,w ) by A2, A3, A7, ANPROJ_1:35;
A13: ( are_Prop t1,t & are_Prop x2,x ) by A4, A6, A7, A8, ANPROJ_1:35;
A14: ( are_Prop z2,z & are_Prop t2,t ) by A2, A6, A8, ANPROJ_1:35;
A15: are_Prop v1,v by A2, A5, ANPROJ_1:35;
thus u,v,z are_LinDep by A2; :: thesis:
thus w,y,z are_LinDep by A3, A9, ANPROJ_1:9; :: thesis:
thus u,w,x are_LinDep by A4, A9, ANPROJ_1:9; :: thesis:
thus v,y,x are_LinDep by A5, A10, A15, ANPROJ_1:9; :: thesis:
thus u,y,t are_LinDep by A6, A11, ANPROJ_1:9; :: thesis:
thus v,w,t are_LinDep by A7, A12, A13, ANPROJ_1:9; :: thesis:
thus x,z,t are_LinDep by A8, A13, A14, ANPROJ_1:9; :: thesis:

end;

then ( u,v,y are_LinDep or u,v,w are_LinDep or u,w,y are_LinDep or v,w,y are_LinDep ) by A2, A4, A6, ANPROJ_1:23;
hence ( p1,r2,q1 is_collinear or p1,r2,r1 is_collinear or p1,r1,q1 is_collinear or r2,r1,q1 is_collinear ) by A2, A3, Th24; :: thesis: