let V be non trivial RealLinearSpace; :: thesis: for p, p1, q, q1, r, r1, r2 being Element of () 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 (); :: 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 ;
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 ;
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 ;
A29: are_Prop w1,w by ;
are_Prop z1,z by ;
then A30: w,y,z are_LinDep by ;
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 ;
A38: are_Prop x2,x by ;
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 ;
A46: are_Prop y2,y by ;
A47: are_Prop t2,t by ;
are_Prop z2,z by ;
then A48: x,z,t are_LinDep by ;
are_Prop u2,u by ;
then A49: u,y,t are_LinDep by ;
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 ;
A57: are_Prop t1,t by ;
are_Prop u1,u by ;
then A58: u,w,x are_LinDep by ;
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 ;
A66: are_Prop x1,x by ;
A67: are_Prop w2,w by ;
are_Prop v2,v by ;
then A68: v,w,t are_LinDep by ;
A69: are_Prop y1,y by ;
are_Prop v1,v by ;
then v,y,x are_LinDep by ;
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 ;
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