let V be non trivial RealLinearSpace; :: thesis:
let p be Element of (); :: according to ANPROJ_2:def 8 :: thesis: for q, r, r1, r2 being Element of () st p <> q & p,q,r are_collinear & p,q,r1 are_collinear & p,q,r2 are_collinear holds
r,r1,r2 are_collinear

let q, r, r1, r2 be Element of (); :: thesis: ( p <> q & p,q,r are_collinear & p,q,r1 are_collinear & p,q,r2 are_collinear implies r,r1,r2 are_collinear )
assume that
A1: p <> q and
A2: p,q,r are_collinear and
A3: p,q,r1 are_collinear and
A4: p,q,r2 are_collinear ; :: thesis: r,r1,r2 are_collinear
consider u1, v1, w1 being Element of V such that
A5: p = Dir u1 and
A6: q = Dir v1 and
A7: r = Dir w1 and
A8: not u1 is zero and
A9: not v1 is zero and
A10: not w1 is zero and
A11: u1,v1,w1 are_LinDep by ;
consider v being Element of V such that
A12: not v is zero and
A13: q = Dir v by ANPROJ_1:26;
A14: are_Prop v1,v by ;
consider u3, v3, w3 being Element of V such that
A15: p = Dir u3 and
A16: q = Dir v3 and
A17: r2 = Dir w3 and
A18: not u3 is zero and
A19: not v3 is zero and
A20: not w3 is zero and
A21: u3,v3,w3 are_LinDep by ;
A22: are_Prop v3,v by ;
consider u2, v2, w2 being Element of V such that
A23: p = Dir u2 and
A24: q = Dir v2 and
A25: r1 = Dir w2 and
A26: not u2 is zero and
A27: not v2 is zero and
A28: not w2 is zero and
A29: u2,v2,w2 are_LinDep by ;
A30: are_Prop v2,v by ;
consider u being Element of V such that
A31: not u is zero and
A32: p = Dir u by ANPROJ_1:26;
are_Prop u1,u by ;
then A33: u,v,w1 are_LinDep by ;
are_Prop u3,u by ;
then A34: u,v,w3 are_LinDep by ;
are_Prop u2,u by ;
then A35: u,v,w2 are_LinDep by ;
not are_Prop u,v by ;
then w1,w2,w3 are_LinDep by ;
hence r,r1,r2 are_collinear by A7, A10, A25, A28, A17, A20, Th23; :: thesis: verum