let V be non trivial RealLinearSpace; for p, p1, p2, r, r1 being Element of (ProjectiveSpace V) st not p,p1,p2 are_collinear & 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 p, p1, p2, r, r1 be Element of (ProjectiveSpace V); ( not p,p1,p2 are_collinear & 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 that
A1:
not p,p1,p2 are_collinear
and
A2:
p,p1,r are_collinear
and
A3:
p1,p2,r1 are_collinear
; ex r2 being Element of (ProjectiveSpace V) st
( p,p2,r2 are_collinear & r,r1,r2 are_collinear )
consider u, v, t being Element of V such that
A4:
p = Dir u
and
A5:
p1 = Dir v
and
A6:
r = Dir t
and
A7:
not u is zero
and
A8:
not v is zero
and
A9:
not t is zero
and
A10:
u,v,t are_LinDep
by A2, Th23;
consider v1, w, s being Element of V such that
A11:
p1 = Dir v1
and
A12:
p2 = Dir w
and
A13:
r1 = Dir s
and
A14:
not v1 is zero
and
A15:
not w is zero
and
A16:
not s is zero
and
A17:
v1,w,s are_LinDep
by A3, Th23;
are_Prop v1,v
by A5, A8, A11, A14, ANPROJ_1:22;
then A18:
v,w,s are_LinDep
by A17, ANPROJ_1:4;
not u,v,w are_LinDep
by A1, A4, A5, A7, A8, A12, A15, Th23;
then consider y being Element of V such that
A19:
( u,w,y are_LinDep & t,s,y are_LinDep )
and
A20:
not y is zero
by A10, A18, ANPROJ_1:15;
reconsider r2 = Dir y as Element of (ProjectiveSpace V) by A20, ANPROJ_1:26;
take
r2
; ( p,p2,r2 are_collinear & r,r1,r2 are_collinear )
thus
( p,p2,r2 are_collinear & r,r1,r2 are_collinear )
by A4, A6, A7, A9, A12, A13, A15, A16, A19, A20, Th23; verum