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 are_collinear & p,p,q are_collinear & p,q,q are_collinear )
let q be Element of (ProjectiveSpace V); :: thesis: for r being Element of (ProjectiveSpace V) holds
( p,q,p are_collinear & p,p,q are_collinear & p,q,q are_collinear )
consider u being Element of V such that
A1: ( not u is zero & p = Dir u ) by ANPROJ_1:26;
consider v being Element of V such that
A2: ( not v is zero & q = Dir v ) by ANPROJ_1:26;
A3: u,v,v are_LinDep by ANPROJ_1:11;
( u,v,u are_LinDep & u,u,v are_LinDep ) by ANPROJ_1:11;
hence for r being Element of (ProjectiveSpace V) holds
( p,q,p are_collinear & p,p,q are_collinear & p,q,q are_collinear ) by A1, A2, A3, Th23; :: thesis: verum