let V be non trivial RealLinearSpace; 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); ( 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
; ( 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; verum