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