let V be non trivial RealLinearSpace; :: thesis: for p, p1, q, q1, r, r1, r2 being Element of (ProjectiveSpace V) st p1,r2,q are_collinear & r1,q1,q are_collinear & p1,r1,p are_collinear & r2,q1,p are_collinear & p1,q1,r are_collinear & r2,r1,r are_collinear & p,q,r are_collinear & not p1,r2,q1 are_collinear & not p1,r2,r1 are_collinear & not p1,r1,q1 are_collinear holds

r2,r1,q1 are_collinear

let p, p1, q, q1, r, r1, r2 be Element of (ProjectiveSpace V); :: thesis: ( p1,r2,q are_collinear & r1,q1,q are_collinear & p1,r1,p are_collinear & r2,q1,p are_collinear & p1,q1,r are_collinear & r2,r1,r are_collinear & p,q,r are_collinear & not p1,r2,q1 are_collinear & not p1,r2,r1 are_collinear & not p1,r1,q1 are_collinear implies r2,r1,q1 are_collinear )

assume that

A1: p1,r2,q are_collinear and

A2: r1,q1,q are_collinear and

A3: p1,r1,p are_collinear and

A4: r2,q1,p are_collinear and

A5: p1,q1,r are_collinear and

A6: r2,r1,r are_collinear and

A7: p,q,r are_collinear ; :: thesis: ( p1,r2,q1 are_collinear or p1,r2,r1 are_collinear or p1,r1,q1 are_collinear or r2,r1,q1 are_collinear )

consider u1, w1, x being Element of V such that

A8: p1 = Dir u1 and

A9: r1 = Dir w1 and

A10: p = Dir x and

A11: not u1 is zero and

A12: not w1 is zero and

A13: not x is zero and

A14: u1,w1,x are_LinDep by A3, Th23;

consider u, v, z being Element of V such that

A15: p1 = Dir u and

A16: r2 = Dir v and

A17: q = Dir z and

A18: not u is zero and

A19: not v is zero and

A20: not z is zero and

A21: u,v,z are_LinDep by A1, Th23;

consider w, y, z1 being Element of V such that

A22: r1 = Dir w and

A23: q1 = Dir y and

A24: q = Dir z1 and

A25: not w is zero and

A26: not y is zero and

A27: not z1 is zero and

A28: w,y,z1 are_LinDep by A2, Th23;

A29: are_Prop w1,w by A22, A25, A9, A12, ANPROJ_1:22;

are_Prop z1,z by A17, A20, A24, A27, ANPROJ_1:22;

then A30: w,y,z are_LinDep by A28, ANPROJ_1:4;

consider x2, z2, t2 being Element of V such that

A31: p = Dir x2 and

A32: q = Dir z2 and

A33: r = Dir t2 and

A34: not x2 is zero and

A35: not z2 is zero and

A36: not t2 is zero and

A37: x2,z2,t2 are_LinDep by A7, Th23;

A38: are_Prop x2,x by A10, A13, A31, A34, ANPROJ_1:22;

consider u2, y2, t being Element of V such that

A39: p1 = Dir u2 and

A40: q1 = Dir y2 and

A41: r = Dir t and

A42: not u2 is zero and

A43: not y2 is zero and

A44: not t is zero and

A45: u2,y2,t are_LinDep by A5, Th23;

A46: are_Prop y2,y by A23, A26, A40, A43, ANPROJ_1:22;

A47: are_Prop t2,t by A41, A44, A33, A36, ANPROJ_1:22;

are_Prop z2,z by A17, A20, A32, A35, ANPROJ_1:22;

then A48: x,z,t are_LinDep by A37, A38, A47, ANPROJ_1:4;

are_Prop u2,u by A15, A18, A39, A42, ANPROJ_1:22;

then A49: u,y,t are_LinDep by A45, A46, ANPROJ_1:4;

consider v2, w2, t1 being Element of V such that

A50: r2 = Dir v2 and

A51: r1 = Dir w2 and

A52: r = Dir t1 and

A53: not v2 is zero and

A54: not w2 is zero and

A55: not t1 is zero and

A56: v2,w2,t1 are_LinDep by A6, Th23;

A57: are_Prop t1,t by A41, A44, A52, A55, ANPROJ_1:22;

are_Prop u1,u by A15, A18, A8, A11, ANPROJ_1:22;

then A58: u,w,x are_LinDep by A14, A29, ANPROJ_1:4;

consider v1, y1, x1 being Element of V such that

A59: r2 = Dir v1 and

A60: q1 = Dir y1 and

A61: p = Dir x1 and

A62: not v1 is zero and

A63: not y1 is zero and

A64: not x1 is zero and

A65: v1,y1,x1 are_LinDep by A4, Th23;

A66: are_Prop x1,x by A10, A13, A61, A64, ANPROJ_1:22;

A67: are_Prop w2,w by A22, A25, A51, A54, ANPROJ_1:22;

are_Prop v2,v by A16, A19, A50, A53, ANPROJ_1:22;

then A68: v,w,t are_LinDep by A56, A67, A57, ANPROJ_1:4;

A69: are_Prop y1,y by A23, A26, A60, A63, ANPROJ_1:22;

are_Prop v1,v by A16, A19, A59, A62, ANPROJ_1:22;

then v,y,x are_LinDep by A65, A69, A66, ANPROJ_1:4;

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 A20, A21, A13, A44, A30, A58, A49, A68, A48, ANPROJ_1:18;

hence ( p1,r2,q1 are_collinear or p1,r2,r1 are_collinear or p1,r1,q1 are_collinear or r2,r1,q1 are_collinear ) by A15, A16, A18, A19, A22, A23, A25, A26, Th23; :: thesis: verum

r2,r1,q1 are_collinear

let p, p1, q, q1, r, r1, r2 be Element of (ProjectiveSpace V); :: thesis: ( p1,r2,q are_collinear & r1,q1,q are_collinear & p1,r1,p are_collinear & r2,q1,p are_collinear & p1,q1,r are_collinear & r2,r1,r are_collinear & p,q,r are_collinear & not p1,r2,q1 are_collinear & not p1,r2,r1 are_collinear & not p1,r1,q1 are_collinear implies r2,r1,q1 are_collinear )

assume that

A1: p1,r2,q are_collinear and

A2: r1,q1,q are_collinear and

A3: p1,r1,p are_collinear and

A4: r2,q1,p are_collinear and

A5: p1,q1,r are_collinear and

A6: r2,r1,r are_collinear and

A7: p,q,r are_collinear ; :: thesis: ( p1,r2,q1 are_collinear or p1,r2,r1 are_collinear or p1,r1,q1 are_collinear or r2,r1,q1 are_collinear )

consider u1, w1, x being Element of V such that

A8: p1 = Dir u1 and

A9: r1 = Dir w1 and

A10: p = Dir x and

A11: not u1 is zero and

A12: not w1 is zero and

A13: not x is zero and

A14: u1,w1,x are_LinDep by A3, Th23;

consider u, v, z being Element of V such that

A15: p1 = Dir u and

A16: r2 = Dir v and

A17: q = Dir z and

A18: not u is zero and

A19: not v is zero and

A20: not z is zero and

A21: u,v,z are_LinDep by A1, Th23;

consider w, y, z1 being Element of V such that

A22: r1 = Dir w and

A23: q1 = Dir y and

A24: q = Dir z1 and

A25: not w is zero and

A26: not y is zero and

A27: not z1 is zero and

A28: w,y,z1 are_LinDep by A2, Th23;

A29: are_Prop w1,w by A22, A25, A9, A12, ANPROJ_1:22;

are_Prop z1,z by A17, A20, A24, A27, ANPROJ_1:22;

then A30: w,y,z are_LinDep by A28, ANPROJ_1:4;

consider x2, z2, t2 being Element of V such that

A31: p = Dir x2 and

A32: q = Dir z2 and

A33: r = Dir t2 and

A34: not x2 is zero and

A35: not z2 is zero and

A36: not t2 is zero and

A37: x2,z2,t2 are_LinDep by A7, Th23;

A38: are_Prop x2,x by A10, A13, A31, A34, ANPROJ_1:22;

consider u2, y2, t being Element of V such that

A39: p1 = Dir u2 and

A40: q1 = Dir y2 and

A41: r = Dir t and

A42: not u2 is zero and

A43: not y2 is zero and

A44: not t is zero and

A45: u2,y2,t are_LinDep by A5, Th23;

A46: are_Prop y2,y by A23, A26, A40, A43, ANPROJ_1:22;

A47: are_Prop t2,t by A41, A44, A33, A36, ANPROJ_1:22;

are_Prop z2,z by A17, A20, A32, A35, ANPROJ_1:22;

then A48: x,z,t are_LinDep by A37, A38, A47, ANPROJ_1:4;

are_Prop u2,u by A15, A18, A39, A42, ANPROJ_1:22;

then A49: u,y,t are_LinDep by A45, A46, ANPROJ_1:4;

consider v2, w2, t1 being Element of V such that

A50: r2 = Dir v2 and

A51: r1 = Dir w2 and

A52: r = Dir t1 and

A53: not v2 is zero and

A54: not w2 is zero and

A55: not t1 is zero and

A56: v2,w2,t1 are_LinDep by A6, Th23;

A57: are_Prop t1,t by A41, A44, A52, A55, ANPROJ_1:22;

are_Prop u1,u by A15, A18, A8, A11, ANPROJ_1:22;

then A58: u,w,x are_LinDep by A14, A29, ANPROJ_1:4;

consider v1, y1, x1 being Element of V such that

A59: r2 = Dir v1 and

A60: q1 = Dir y1 and

A61: p = Dir x1 and

A62: not v1 is zero and

A63: not y1 is zero and

A64: not x1 is zero and

A65: v1,y1,x1 are_LinDep by A4, Th23;

A66: are_Prop x1,x by A10, A13, A61, A64, ANPROJ_1:22;

A67: are_Prop w2,w by A22, A25, A51, A54, ANPROJ_1:22;

are_Prop v2,v by A16, A19, A50, A53, ANPROJ_1:22;

then A68: v,w,t are_LinDep by A56, A67, A57, ANPROJ_1:4;

A69: are_Prop y1,y by A23, A26, A60, A63, ANPROJ_1:22;

are_Prop v1,v by A16, A19, A59, A62, ANPROJ_1:22;

then v,y,x are_LinDep by A65, A69, A66, ANPROJ_1:4;

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 A20, A21, A13, A44, A30, A58, A49, A68, A48, ANPROJ_1:18;

hence ( p1,r2,q1 are_collinear or p1,r2,r1 are_collinear or p1,r1,q1 are_collinear or r2,r1,q1 are_collinear ) by A15, A16, A18, A19, A22, A23, A25, A26, Th23; :: thesis: verum