let V be non trivial RealLinearSpace; :: thesis: for p, q, r being Element of (ProjectiveSpace V) 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 (ProjectiveSpace V); :: 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 A2, ANPROJ_1:5;
A4: v,w,u are_LinDep by A2, ANPROJ_1:5;
( u,w,v are_LinDep & v,u,w are_LinDep ) by A2, ANPROJ_1:5;
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