let PCPP be CollProjectiveSpace; :: thesis: ( PCPP is Pappian implies PCPP is Desarguesian )
assume A1: PCPP is Pappian ; :: thesis: PCPP is Desarguesian
A2: now :: thesis: ( ( 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 ) ; :: thesis: 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; :: thesis: verum
end;
now :: thesis: ( ex p, p1, q, q1 being Element of PCPP st
for r being Element of PCPP holds
( not p,p1,r are_collinear or not q,q1,r are_collinear ) implies PCPP is Desarguesian )
assume ex p, p1, q, q1 being Element of PCPP st
for r being Element of PCPP holds
( not p,p1,r are_collinear or not q,q1,r are_collinear ) ; :: thesis: PCPP is Desarguesian
then PCPP is up-3-dimensional CollProjectiveSpace by ANPROJ_2:def 14;
hence PCPP is Desarguesian ; :: thesis: verum
end;
hence PCPP is Desarguesian by A2; :: thesis: verum