let V be non trivial RealLinearSpace; for p, p1, q, q1, r, r1, r2 being Element of (ProjectiveSpace V) st p1,r2,q are_collinear & r1,q1,q are_collinear & p1,r1,p are_collinear & r2,q1,p are_collinear & p1,q1,r are_collinear & r2,r1,r are_collinear & p,q,r are_collinear & not p1,r2,q1 are_collinear & not p1,r2,r1 are_collinear & not p1,r1,q1 are_collinear holds
r2,r1,q1 are_collinear
let p, p1, q, q1, r, r1, r2 be Element of (ProjectiveSpace V); ( p1,r2,q are_collinear & r1,q1,q are_collinear & p1,r1,p are_collinear & r2,q1,p are_collinear & p1,q1,r are_collinear & r2,r1,r are_collinear & p,q,r are_collinear & not p1,r2,q1 are_collinear & not p1,r2,r1 are_collinear & not p1,r1,q1 are_collinear implies r2,r1,q1 are_collinear )
assume that
A1:
p1,r2,q are_collinear
and
A2:
r1,q1,q are_collinear
and
A3:
p1,r1,p are_collinear
and
A4:
r2,q1,p are_collinear
and
A5:
p1,q1,r are_collinear
and
A6:
r2,r1,r are_collinear
and
A7:
p,q,r are_collinear
; ( p1,r2,q1 are_collinear or p1,r2,r1 are_collinear or p1,r1,q1 are_collinear or r2,r1,q1 are_collinear )
consider u1, w1, x being Element of V such that
A8:
p1 = Dir u1
and
A9:
r1 = Dir w1
and
A10:
p = Dir x
and
A11:
not u1 is zero
and
A12:
not w1 is zero
and
A13:
not x is zero
and
A14:
u1,w1,x are_LinDep
by A3, Th23;
consider u, v, z being Element of V such that
A15:
p1 = Dir u
and
A16:
r2 = Dir v
and
A17:
q = Dir z
and
A18:
not u is zero
and
A19:
not v is zero
and
A20:
not z is zero
and
A21:
u,v,z are_LinDep
by A1, Th23;
consider w, y, z1 being Element of V such that
A22:
r1 = Dir w
and
A23:
q1 = Dir y
and
A24:
q = Dir z1
and
A25:
not w is zero
and
A26:
not y is zero
and
A27:
not z1 is zero
and
A28:
w,y,z1 are_LinDep
by A2, Th23;
A29:
are_Prop w1,w
by A22, A25, A9, A12, ANPROJ_1:22;
are_Prop z1,z
by A17, A20, A24, A27, ANPROJ_1:22;
then A30:
w,y,z are_LinDep
by A28, ANPROJ_1:4;
consider x2, z2, t2 being Element of V such that
A31:
p = Dir x2
and
A32:
q = Dir z2
and
A33:
r = Dir t2
and
A34:
not x2 is zero
and
A35:
not z2 is zero
and
A36:
not t2 is zero
and
A37:
x2,z2,t2 are_LinDep
by A7, Th23;
A38:
are_Prop x2,x
by A10, A13, A31, A34, ANPROJ_1:22;
consider u2, y2, t being Element of V such that
A39:
p1 = Dir u2
and
A40:
q1 = Dir y2
and
A41:
r = Dir t
and
A42:
not u2 is zero
and
A43:
not y2 is zero
and
A44:
not t is zero
and
A45:
u2,y2,t are_LinDep
by A5, Th23;
A46:
are_Prop y2,y
by A23, A26, A40, A43, ANPROJ_1:22;
A47:
are_Prop t2,t
by A41, A44, A33, A36, ANPROJ_1:22;
are_Prop z2,z
by A17, A20, A32, A35, ANPROJ_1:22;
then A48:
x,z,t are_LinDep
by A37, A38, A47, ANPROJ_1:4;
are_Prop u2,u
by A15, A18, A39, A42, ANPROJ_1:22;
then A49:
u,y,t are_LinDep
by A45, A46, ANPROJ_1:4;
consider v2, w2, t1 being Element of V such that
A50:
r2 = Dir v2
and
A51:
r1 = Dir w2
and
A52:
r = Dir t1
and
A53:
not v2 is zero
and
A54:
not w2 is zero
and
A55:
not t1 is zero
and
A56:
v2,w2,t1 are_LinDep
by A6, Th23;
A57:
are_Prop t1,t
by A41, A44, A52, A55, ANPROJ_1:22;
are_Prop u1,u
by A15, A18, A8, A11, ANPROJ_1:22;
then A58:
u,w,x are_LinDep
by A14, A29, ANPROJ_1:4;
consider v1, y1, x1 being Element of V such that
A59:
r2 = Dir v1
and
A60:
q1 = Dir y1
and
A61:
p = Dir x1
and
A62:
not v1 is zero
and
A63:
not y1 is zero
and
A64:
not x1 is zero
and
A65:
v1,y1,x1 are_LinDep
by A4, Th23;
A66:
are_Prop x1,x
by A10, A13, A61, A64, ANPROJ_1:22;
A67:
are_Prop w2,w
by A22, A25, A51, A54, ANPROJ_1:22;
are_Prop v2,v
by A16, A19, A50, A53, ANPROJ_1:22;
then A68:
v,w,t are_LinDep
by A56, A67, A57, ANPROJ_1:4;
A69:
are_Prop y1,y
by A23, A26, A60, A63, ANPROJ_1:22;
are_Prop v1,v
by A16, A19, A59, A62, ANPROJ_1:22;
then
v,y,x are_LinDep
by A65, A69, A66, ANPROJ_1:4;
then
( u,v,y are_LinDep or u,v,w are_LinDep or u,w,y are_LinDep or v,w,y are_LinDep )
by A20, A21, A13, A44, A30, A58, A49, A68, A48, ANPROJ_1:18;
hence
( p1,r2,q1 are_collinear or p1,r2,r1 are_collinear or p1,r1,q1 are_collinear or r2,r1,q1 are_collinear )
by A15, A16, A18, A19, A22, A23, A25, A26, Th23; verum