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

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