let V be non trivial RealLinearSpace; :: thesis: for p, q, r being Element of () st p,q,r are_collinear holds
( p,r,q are_collinear & q,p,r are_collinear & r,q,p are_collinear & r,p,q are_collinear & q,r,p are_collinear )

let p, q, r be Element of (); :: thesis: ( p,q,r are_collinear implies ( p,r,q are_collinear & q,p,r are_collinear & r,q,p are_collinear & r,p,q are_collinear & q,r,p are_collinear ) )
assume p,q,r are_collinear ; :: thesis: ( p,r,q are_collinear & q,p,r are_collinear & r,q,p are_collinear & r,p,q are_collinear & q,r,p are_collinear )
then consider u, v, w being Element of V such that
A1: ( p = Dir u & q = Dir v & r = Dir w & not u is zero & not v is zero & not w is zero ) and
A2: u,v,w are_LinDep by Th23;
A3: ( w,v,u are_LinDep & w,u,v are_LinDep ) by ;
A4: v,w,u are_LinDep by ;
( u,w,v are_LinDep & v,u,w are_LinDep ) by ;
hence ( p,r,q are_collinear & q,p,r are_collinear & r,q,p are_collinear & r,p,q are_collinear & q,r,p are_collinear ) by A1, A3, A4, Th23; :: thesis: verum