begin
theorem Th1:
for
PCPP being
CollProjectiveSpace for
a,
b,
c being
Element of
PCPP st
a,
b,
c is_collinear holds
(
b,
c,
a is_collinear &
c,
a,
b is_collinear &
b,
a,
c is_collinear &
a,
c,
b is_collinear &
c,
b,
a is_collinear )
theorem
for
PCPP being
CollProjectiveSpace for
p,
q,
a,
b,
r being
Element of
PCPP st
p <> q &
a,
b,
p is_collinear &
a,
b,
q is_collinear &
p,
q,
r is_collinear holds
a,
b,
r is_collinear
theorem Th8:
for
PCPP being
CollProjectiveSpace for
o,
a,
d,
d9,
a9,
x being
Element of
PCPP st not
o,
a,
d is_collinear &
o,
d,
d9 is_collinear &
d <> d9 &
a9,
d9,
x is_collinear &
o,
a,
a9 is_collinear &
o <> a9 holds
x <> d
theorem Th9:
for
PCPP being
CollProjectiveSpace for
a1,
a2,
a3,
c3,
c1,
x being
Element of
PCPP st not
a1,
a2,
a3 is_collinear &
a1,
a2,
c3 is_collinear &
a2,
a3,
c1 is_collinear &
c1,
c3,
x is_collinear &
c3 <> a1 &
c3 <> a2 &
c1 <> a2 &
c1 <> a3 holds
(
a1 <> x &
a3 <> x )
theorem Th10:
for
PCPP being
CollProjectiveSpace for
a,
b,
c,
d,
e being
Element of
PCPP st not
a,
b,
c is_collinear &
a,
b,
d is_collinear &
c,
e,
d is_collinear &
e <> c &
d <> a holds
not
e,
a,
c is_collinear
theorem Th11:
for
PCPP being
CollProjectiveSpace for
p1,
p2,
q1,
q2,
q3 being
Element of
PCPP st not
p1,
p2,
q1 is_collinear &
p1,
p2,
q2 is_collinear &
q1,
q2,
q3 is_collinear &
q2 <> q3 holds
not
p2,
p1,
q3 is_collinear
theorem
for
PCPP being
CollProjectiveSpace for
p1,
p2,
q1,
p3,
q2 being
Element of
PCPP st not
p1,
p2,
q1 is_collinear &
p1,
p2,
p3 is_collinear &
q1,
q2,
p3 is_collinear &
p3 <> q2 &
p2 <> p3 holds
not
p3,
p2,
q2 is_collinear
theorem Th13:
for
PCPP being
CollProjectiveSpace for
p1,
p2,
q1,
p3,
q2 being
Element of
PCPP st not
p1,
p2,
q1 is_collinear &
p1,
p2,
p3 is_collinear &
q1,
q2,
p1 is_collinear &
p1 <> p3 &
p1 <> q2 holds
not
p3,
p1,
q2 is_collinear
theorem Th14:
for
PCPP being
CollProjectiveSpace for
a1,
a2,
b1,
b2,
x,
y being
Element of
PCPP st
a1 <> a2 &
b1 <> b2 &
b1,
b2,
x is_collinear &
b1,
b2,
y is_collinear &
a1,
a2,
x is_collinear &
a1,
a2,
y is_collinear & not
a1,
a2,
b1 is_collinear holds
x = y
theorem Th15:
for
PCPP being
CollProjectiveSpace for
o,
a1,
a2,
b1,
b2 being
Element of
PCPP st not
o,
a1,
a2 is_collinear &
o,
a1,
b1 is_collinear &
o,
a2,
b2 is_collinear &
o <> b1 &
o <> b2 holds
not
o,
b1,
b2 is_collinear
theorem Th16:
for
PCPP being
Pappian CollProjectivePlane for
p2,
p3,
p1,
q2,
q3,
q1,
r3,
r2,
r1 being
Element of
PCPP st
p2 <> p3 &
p1 <> p3 &
q2 <> q3 &
q1 <> q2 &
q1 <> q3 & not
p1,
p2,
q1 is_collinear &
p1,
p2,
p3 is_collinear &
q1,
q2,
q3 is_collinear &
p1,
q2,
r3 is_collinear &
q1,
p2,
r3 is_collinear &
p1,
q3,
r2 is_collinear &
p3,
q1,
r2 is_collinear &
p2,
q3,
r1 is_collinear &
p3,
q2,
r1 is_collinear holds
r1,
r2,
r3 is_collinear
Lm1:
for PCPP being Pappian CollProjectivePlane
for o, b1, b2, a1, a2, a3, c3, c1, b3, c2 being Element of PCPP st o <> b1 & o <> b2 & not o,a1,a2 is_collinear & not o,a1,a3 is_collinear & not o,a2,a3 is_collinear & a1,a2,c3 is_collinear & b1,b2,c3 is_collinear & a2,a3,c1 is_collinear & b2,b3,c1 is_collinear & a1,a3,c2 is_collinear & b1,b3,c2 is_collinear & o,a1,b1 is_collinear & o,a2,b2 is_collinear & o,a3,b3 is_collinear & ( a1,a2,a3 is_collinear or b1,b2,b3 is_collinear ) holds
c1,c2,c3 is_collinear
Lm2:
for PCPP being Pappian CollProjectivePlane
for o, b1, a1, b2, a2, b3, a3, c1, c3, c2, x being Element of PCPP st o <> b1 & a1 <> b1 & o <> b2 & a2 <> b2 & o <> b3 & a3 <> b3 & not o,a1,a2 is_collinear & not o,a1,a3 is_collinear & not o,a2,a3 is_collinear & not o,c1,c3 is_collinear & a1,a2,c3 is_collinear & b1,b2,c3 is_collinear & a2,a3,c1 is_collinear & b2,b3,c1 is_collinear & a1,a3,c2 is_collinear & b1,b3,c2 is_collinear & o,a1,b1 is_collinear & o,a2,b2 is_collinear & o,a3,b3 is_collinear & o,a2,x is_collinear & a1,a3,x is_collinear & not c1,c3,x is_collinear holds
c1,c2,c3 is_collinear
Lm3:
for PCPP being Pappian CollProjectivePlane
for o, b1, a1, b2, a2, b3, a3, c1, c3, c2 being Element of PCPP st o <> b1 & a1 <> b1 & o <> b2 & a2 <> b2 & o <> b3 & a3 <> b3 & not o,a1,a2 is_collinear & not o,a1,a3 is_collinear & not o,a2,a3 is_collinear & not o,c1,c3 is_collinear & a1,a2,c3 is_collinear & b1,b2,c3 is_collinear & a2,a3,c1 is_collinear & b2,b3,c1 is_collinear & a1,a3,c2 is_collinear & b1,b3,c2 is_collinear & o,a1,b1 is_collinear & o,a2,b2 is_collinear & o,a3,b3 is_collinear holds
c1,c2,c3 is_collinear
theorem Th17:
for
PCPP being
Pappian CollProjectivePlane for
o,
b1,
a1,
b2,
a2,
b3,
a3,
c3,
c1,
c2 being
Element of
PCPP st
o <> b1 &
a1 <> b1 &
o <> b2 &
a2 <> b2 &
o <> b3 &
a3 <> b3 & not
o,
a1,
a2 is_collinear & not
o,
a1,
a3 is_collinear & not
o,
a2,
a3 is_collinear &
a1,
a2,
c3 is_collinear &
b1,
b2,
c3 is_collinear &
a2,
a3,
c1 is_collinear &
b2,
b3,
c1 is_collinear &
a1,
a3,
c2 is_collinear &
b1,
b3,
c2 is_collinear &
o,
a1,
b1 is_collinear &
o,
a2,
b2 is_collinear &
o,
a3,
b3 is_collinear holds
c1,
c2,
c3 is_collinear