let V be non trivial RealLinearSpace; :: thesis: ProjectiveSpace V is reflexive
let p be Element of ; :: according to ANPROJ_2:def 7 :: thesis: for q, r being Element of holds
( p,q,p is_collinear & p,p,q is_collinear & p,q,q is_collinear )
let q be Element of ; :: thesis: for r being Element of holds
( p,q,p is_collinear & p,p,q is_collinear & p,q,q is_collinear )
consider u being Element of such that
A1: ( not u is zero & p = Dir u ) by ANPROJ_1:42;
consider v being Element of such that
A2: ( not v is zero & q = Dir v ) by ANPROJ_1:42;
A3: u,v,v are_LinDep by ANPROJ_1:16;
( u,v,u are_LinDep & u,u,v are_LinDep ) by ANPROJ_1:16;
hence for r being Element of holds
( p,q,p is_collinear & p,p,q is_collinear & p,q,q is_collinear ) by A1, A2, A3, Th24; :: thesis: verum