let PCPP be CollProjectiveSpace; ( PCPP is Pappian implies PCPP is Desarguesian )
assume A1:
PCPP is Pappian
; PCPP is Desarguesian
A2:
now ( ( for p, p1, q, q1 being Element of PCPP ex r being Element of PCPP st
( p,p1,r are_collinear & q,q1,r are_collinear ) ) implies PCPP is Desarguesian )assume
for
p,
p1,
q,
q1 being
Element of
PCPP ex
r being
Element of
PCPP st
(
p,
p1,
r are_collinear &
q,
q1,
r are_collinear )
;
PCPP is Desarguesian then
PCPP is
Pappian CollProjectivePlane
by A1, ANPROJ_2:def 14;
then
for
o,
p1,
p2,
p3,
q1,
q2,
q3,
r1,
r2,
r3 being
Element of
PCPP st
o <> q1 &
p1 <> q1 &
o <> q2 &
p2 <> q2 &
o <> q3 &
p3 <> q3 & not
o,
p1,
p2 are_collinear & not
o,
p1,
p3 are_collinear & not
o,
p2,
p3 are_collinear &
p1,
p2,
r3 are_collinear &
q1,
q2,
r3 are_collinear &
p2,
p3,
r1 are_collinear &
q2,
q3,
r1 are_collinear &
p1,
p3,
r2 are_collinear &
q1,
q3,
r2 are_collinear &
o,
p1,
q1 are_collinear &
o,
p2,
q2 are_collinear &
o,
p3,
q3 are_collinear holds
r1,
r2,
r3 are_collinear
by Th17;
hence
PCPP is
Desarguesian
by ANPROJ_2:def 12;
verum end;
hence
PCPP is Desarguesian
by A2; verum