let V be non trivial RealLinearSpace; :: thesis: ProjectiveSpace V is Vebleian
let p be Element of (ProjectiveSpace V); :: according to ANPROJ_2:def 9 :: thesis: for p1, p2, r, r1 being Element of (ProjectiveSpace V) st p,p1,r are_collinear & p1,p2,r1 are_collinear holds
ex r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 are_collinear & r,r1,r2 are_collinear )
let p1, p2, r, r1 be Element of (ProjectiveSpace V); :: thesis: ( p,p1,r are_collinear & p1,p2,r1 are_collinear implies ex r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 are_collinear & r,r1,r2 are_collinear ) )
assume A1: ( p,p1,r are_collinear & p1,p2,r1 are_collinear ) ; :: thesis: ex r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 are_collinear & r,r1,r2 are_collinear )
then ( p,p1,p2 are_collinear implies ex r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 are_collinear & r,r1,r2 are_collinear ) ) by Lm34;
hence ex r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 are_collinear & r,r1,r2 are_collinear ) by A1, Lm35; :: thesis: verum