let V be non trivial RealLinearSpace; ProjectiveSpace V is transitive
let p be Element of (ProjectiveSpace V); ANPROJ_2:def 8 for q, r, r1, r2 being Element of (ProjectiveSpace V) st p <> q & p,q,r are_collinear & p,q,r1 are_collinear & p,q,r2 are_collinear holds
r,r1,r2 are_collinear
let q, r, r1, r2 be Element of (ProjectiveSpace V); ( p <> q & p,q,r are_collinear & p,q,r1 are_collinear & p,q,r2 are_collinear implies r,r1,r2 are_collinear )
assume that
A1:
p <> q
and
A2:
p,q,r are_collinear
and
A3:
p,q,r1 are_collinear
and
A4:
p,q,r2 are_collinear
; r,r1,r2 are_collinear
consider u1, v1, w1 being Element of V such that
A5:
p = Dir u1
and
A6:
q = Dir v1
and
A7:
r = Dir w1
and
A8:
not u1 is zero
and
A9:
not v1 is zero
and
A10:
not w1 is zero
and
A11:
u1,v1,w1 are_LinDep
by A2, Th23;
consider v being Element of V such that
A12:
not v is zero
and
A13:
q = Dir v
by ANPROJ_1:26;
A14:
are_Prop v1,v
by A12, A13, A6, A9, ANPROJ_1:22;
consider u3, v3, w3 being Element of V such that
A15:
p = Dir u3
and
A16:
q = Dir v3
and
A17:
r2 = Dir w3
and
A18:
not u3 is zero
and
A19:
not v3 is zero
and
A20:
not w3 is zero
and
A21:
u3,v3,w3 are_LinDep
by A4, Th23;
A22:
are_Prop v3,v
by A12, A13, A16, A19, ANPROJ_1:22;
consider u2, v2, w2 being Element of V such that
A23:
p = Dir u2
and
A24:
q = Dir v2
and
A25:
r1 = Dir w2
and
A26:
not u2 is zero
and
A27:
not v2 is zero
and
A28:
not w2 is zero
and
A29:
u2,v2,w2 are_LinDep
by A3, Th23;
A30:
are_Prop v2,v
by A12, A13, A24, A27, ANPROJ_1:22;
consider u being Element of V such that
A31:
not u is zero
and
A32:
p = Dir u
by ANPROJ_1:26;
are_Prop u1,u
by A31, A32, A5, A8, ANPROJ_1:22;
then A33:
u,v,w1 are_LinDep
by A11, A14, ANPROJ_1:4;
are_Prop u3,u
by A31, A32, A15, A18, ANPROJ_1:22;
then A34:
u,v,w3 are_LinDep
by A21, A22, ANPROJ_1:4;
are_Prop u2,u
by A31, A32, A23, A26, ANPROJ_1:22;
then A35:
u,v,w2 are_LinDep
by A29, A30, ANPROJ_1:4;
not are_Prop u,v
by A1, A31, A32, A12, A13, ANPROJ_1:22;
then
w1,w2,w3 are_LinDep
by A31, A12, A33, A35, A34, ANPROJ_1:14;
hence
r,r1,r2 are_collinear
by A7, A10, A25, A28, A17, A20, Th23; verum