let V be non trivial RealLinearSpace; :: thesis: for p, p1, p2, r, r1 being Element of (ProjectiveSpace V) st not p,p1,p2 is_collinear & p,p1,r is_collinear & p1,p2,r1 is_collinear holds
ex r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 is_collinear & r,r1,r2 is_collinear )
let p, p1, p2, r, r1 be Element of (ProjectiveSpace V); :: thesis: ( not p,p1,p2 is_collinear & p,p1,r is_collinear & p1,p2,r1 is_collinear implies ex r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 is_collinear & r,r1,r2 is_collinear ) )
assume that
A1: not p,p1,p2 is_collinear and
A2: ( p,p1,r is_collinear & p1,p2,r1 is_collinear ) ; :: thesis: ex r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 is_collinear & r,r1,r2 is_collinear )
consider u, v, t being Element of V such that
A3: ( p = Dir u & p1 = Dir v & r = Dir t & not u is zero & not v is zero & not t is zero & u,v,t are_LinDep ) by A2, Th24;
consider v1, w, s being Element of V such that
A4: ( p1 = Dir v1 & p2 = Dir w & r1 = Dir s & not v1 is zero & not w is zero & not s is zero & v1,w,s are_LinDep ) by A2, Th24;
( are_Prop v1,v & are_Prop w,w & are_Prop s,s ) by A3, A4, ANPROJ_1:35;
then A5: v,w,s are_LinDep by A4, ANPROJ_1:9;
not u,v,w are_LinDep by A1, A3, A4, Th24;
then consider y being Element of V such that
A6: ( u,w,y are_LinDep & t,s,y are_LinDep & not y is zero ) by A3, A5, ANPROJ_1:20;
reconsider r2 = Dir y as Element of (ProjectiveSpace V) by A6, ANPROJ_1:42;
take r2 ; :: thesis: ( p,p2,r2 is_collinear & r,r1,r2 is_collinear )
thus ( p,p2,r2 is_collinear & r,r1,r2 is_collinear ) by A3, A4, A6, Th24; :: thesis: verum