let V be up-3-dimensional RealLinearSpace; ProjectiveSpace V is Pappian
let o, p1, p2, p3, q1, q2, q3, r1, r2, r3 be Element of (ProjectiveSpace V); ANPROJ_2:def 13 ( o <> p2 & o <> p3 & p2 <> p3 & p1 <> p2 & p1 <> p3 & o <> q2 & o <> q3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not o,p1,q1 are_collinear & o,p1,p2 are_collinear & o,p1,p3 are_collinear & o,q1,q2 are_collinear & o,q1,q3 are_collinear & p1,q2,r3 are_collinear & q1,p2,r3 are_collinear & p1,q3,r2 are_collinear & p3,q1,r2 are_collinear & p2,q3,r1 are_collinear & p3,q2,r1 are_collinear implies r1,r2,r3 are_collinear )
assume that
A1:
o <> p2
and
A2:
o <> p3
and
A3:
p2 <> p3
and
A4:
p1 <> p2
and
A5:
p1 <> p3
and
A6:
o <> q2
and
A7:
o <> q3
and
A8:
q2 <> q3
and
A9:
q1 <> q2
and
A10:
q1 <> q3
and
A11:
not o,p1,q1 are_collinear
and
A12:
o,p1,p2 are_collinear
and
A13:
o,p1,p3 are_collinear
and
A14:
o,q1,q2 are_collinear
and
A15:
o,q1,q3 are_collinear
and
A16:
p1,q2,r3 are_collinear
and
A17:
q1,p2,r3 are_collinear
and
A18:
p1,q3,r2 are_collinear
and
A19:
p3,q1,r2 are_collinear
and
A20:
p2,q3,r1 are_collinear
and
A21:
p3,q2,r1 are_collinear
; r1,r2,r3 are_collinear
consider o999, q19, q29 being Element of V such that
A22:
o = Dir o999
and
A23:
q1 = Dir q19
and
A24:
q2 = Dir q29
and
A25:
not o999 is zero
and
A26:
not q19 is zero
and
A27:
not q29 is zero
and
A28:
o999,q19,q29 are_LinDep
by A14, Th23;
A29:
not are_Prop q19,q29
by A9, A23, A24, A26, A27, ANPROJ_1:22;
consider o9999, q199, q39 being Element of V such that
A30:
o = Dir o9999
and
A31:
q1 = Dir q199
and
A32:
q3 = Dir q39
and
A33:
not o9999 is zero
and
A34:
not q199 is zero
and
A35:
not q39 is zero
and
A36:
o9999,q199,q39 are_LinDep
by A15, Th23;
A37:
are_Prop q199,q19
by A23, A26, A31, A34, ANPROJ_1:22;
consider o99, p199, p39 being Element of V such that
A38:
( o = Dir o99 & p1 = Dir p199 )
and
A39:
p3 = Dir p39
and
A40:
( not o99 is zero & not p199 is zero )
and
A41:
not p39 is zero
and
A42:
o99,p199,p39 are_LinDep
by A13, Th23;
consider o9, p19, p29 being Element of V such that
A43:
o = Dir o9
and
A44:
p1 = Dir p19
and
A45:
p2 = Dir p29
and
A46:
not o9 is zero
and
A47:
not p19 is zero
and
A48:
not p29 is zero
and
A49:
o9,p19,p29 are_LinDep
by A12, Th23;
A50:
( not are_Prop o9,p39 & not are_Prop p19,p39 )
by A2, A5, A43, A44, A46, A47, A39, A41, ANPROJ_1:22;
A51:
( not are_Prop q19,q39 & not are_Prop q29,q39 )
by A8, A10, A23, A24, A26, A27, A32, A35, ANPROJ_1:22;
A52:
not are_Prop p29,p39
by A3, A45, A48, A39, A41, ANPROJ_1:22;
A53:
not are_Prop o9,q39
by A7, A43, A46, A32, A35, ANPROJ_1:22;
A54:
not are_Prop o9,q29
by A6, A43, A46, A24, A27, ANPROJ_1:22;
( not are_Prop o9,p29 & not are_Prop p19,p29 )
by A1, A4, A43, A44, A45, A46, A47, A48, ANPROJ_1:22;
then A55:
o9,p19,p29,p39,q19,q29,q39 are_half_mutually_not_Prop
by A54, A53, A50, A29, A52, A51;
consider q1999, p2999, r399 being Element of V such that
A56:
q1 = Dir q1999
and
A57:
p2 = Dir p2999
and
A58:
r3 = Dir r399
and
A59:
not q1999 is zero
and
A60:
not p2999 is zero
and
A61:
not r399 is zero
and
A62:
q1999,p2999,r399 are_LinDep
by A17, Th23;
A63:
are_Prop q1999,q19
by A23, A26, A56, A59, ANPROJ_1:22;
consider p29999, q3999, r19 being Element of V such that
A64:
p2 = Dir p29999
and
A65:
q3 = Dir q3999
and
A66:
r1 = Dir r19
and
A67:
not p29999 is zero
and
A68:
not q3999 is zero
and
A69:
not r19 is zero
and
A70:
p29999,q3999,r19 are_LinDep
by A20, Th23;
A71:
are_Prop q3999,q39
by A32, A35, A65, A68, ANPROJ_1:22;
are_Prop o999,o9
by A43, A46, A22, A25, ANPROJ_1:22;
then A72:
o9,q19,q29 are_LinDep
by A28, ANPROJ_1:4;
are_Prop o9999,o9
by A43, A46, A30, A33, ANPROJ_1:22;
then A73:
o9,q19,q39 are_LinDep
by A36, A37, ANPROJ_1:4;
( are_Prop o99,o9 & are_Prop p199,p19 )
by A43, A44, A46, A47, A38, A40, ANPROJ_1:22;
then A74:
o9,p19,p39 are_LinDep
by A42, ANPROJ_1:4;
not o9,p19,q19 are_LinDep
by A11, A43, A44, A46, A47, A23, A26, Th23;
then A75:
o9,p19,p29,p39,q19,q29,q39 lie_on_an_angle
by A49, A74, A72, A73;
consider p19999, q399, r29 being Element of V such that
A76:
p1 = Dir p19999
and
A77:
q3 = Dir q399
and
A78:
r2 = Dir r29
and
A79:
not p19999 is zero
and
A80:
not q399 is zero
and
A81:
not r29 is zero
and
A82:
p19999,q399,r29 are_LinDep
by A18, Th23;
A83:
are_Prop q399,q39
by A32, A35, A77, A80, ANPROJ_1:22;
consider p3999, q29999, r199 being Element of V such that
A84:
p3 = Dir p3999
and
A85:
q2 = Dir q29999
and
A86:
r1 = Dir r199
and
A87:
not p3999 is zero
and
A88:
not q29999 is zero
and
A89:
not r199 is zero
and
A90:
p3999,q29999,r199 are_LinDep
by A21, Th23;
A91:
are_Prop p3999,p39
by A39, A41, A84, A87, ANPROJ_1:22;
A92:
are_Prop q29999,q29
by A24, A27, A85, A88, ANPROJ_1:22;
are_Prop r199,r19
by A66, A69, A86, A89, ANPROJ_1:22;
then A93:
p39,q29,r19 are_LinDep
by A90, A91, A92, ANPROJ_1:4;
A94:
q19,q29,q39 are_Prop_Vect
by A26, A27, A35;
A95:
p19,p29,p39 are_Prop_Vect
by A47, A48, A41;
are_Prop p29999,p29
by A45, A48, A64, A67, ANPROJ_1:22;
then A96:
p29,q39,r19 are_LinDep
by A70, A71, ANPROJ_1:4;
consider p399, q1999, r299 being Element of V such that
A97:
p3 = Dir p399
and
A98:
q1 = Dir q1999
and
A99:
r2 = Dir r299
and
A100:
not p399 is zero
and
A101:
not q1999 is zero
and
A102:
not r299 is zero
and
A103:
p399,q1999,r299 are_LinDep
by A19, Th23;
A104:
are_Prop q1999,q19
by A23, A26, A98, A101, ANPROJ_1:22;
are_Prop p19999,p19
by A44, A47, A76, A79, ANPROJ_1:22;
then A105:
p19,q39,r29 are_LinDep
by A82, A83, ANPROJ_1:4;
consider p1999, q2999, r39 being Element of V such that
A106:
p1 = Dir p1999
and
A107:
q2 = Dir q2999
and
A108:
r3 = Dir r39
and
A109:
not p1999 is zero
and
A110:
not q2999 is zero
and
A111:
not r39 is zero
and
A112:
p1999,q2999,r39 are_LinDep
by A16, Th23;
A113:
are_Prop q2999,q29
by A24, A27, A107, A110, ANPROJ_1:22;
A114:
are_Prop p2999,p29
by A45, A48, A57, A60, ANPROJ_1:22;
are_Prop r399,r39
by A108, A111, A58, A61, ANPROJ_1:22;
then A115:
q19,p29,r39 are_LinDep
by A62, A63, A114, ANPROJ_1:4;
are_Prop p1999,p19
by A44, A47, A106, A109, ANPROJ_1:22;
then A116:
p19,q29,r39 are_LinDep
by A112, A113, ANPROJ_1:4;
A117:
are_Prop p399,p39
by A39, A41, A97, A100, ANPROJ_1:22;
are_Prop r299,r29
by A78, A81, A99, A102, ANPROJ_1:22;
then A118:
p39,q19,r29 are_LinDep
by A103, A117, A104, ANPROJ_1:4;
r19,r29,r39 are_Prop_Vect
by A111, A81, A69;
then
r19,r29,r39 are_LinDep
by A46, A75, A55, A95, A94, A116, A115, A105, A118, A96, A93, Th9;
hence
r1,r2,r3 are_collinear
by A108, A111, A78, A81, A66, A69, Th23; verum