let V be non trivial RealLinearSpace; :: thesis: for p, q, r being Element of (ProjectiveSpace V) st p,q,r is_collinear holds
( p,r,q is_collinear & q,p,r is_collinear & r,q,p is_collinear & r,p,q is_collinear & q,r,p is_collinear )
let p, q, r be Element of (ProjectiveSpace V); :: thesis: ( p,q,r is_collinear implies ( p,r,q is_collinear & q,p,r is_collinear & r,q,p is_collinear & r,p,q is_collinear & q,r,p is_collinear ) )
assume p,q,r is_collinear ; :: thesis: ( p,r,q is_collinear & q,p,r is_collinear & r,q,p is_collinear & r,p,q is_collinear & q,r,p is_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 & u,v,w are_LinDep ) by Th24;
( u,w,v are_LinDep & v,u,w are_LinDep & w,v,u are_LinDep & w,u,v are_LinDep & v,w,u are_LinDep ) by A1, ANPROJ_1:10;
hence ( p,r,q is_collinear & q,p,r is_collinear & r,q,p is_collinear & r,p,q is_collinear & q,r,p is_collinear ) by A1, Th24; :: thesis: verum