let AS be AffinSpace; :: thesis: ( AS is not AffinPlane implies AS is Desarguesian )

assume AS is not AffinPlane ; :: thesis: AS is Desarguesian

then for A, P, C being Subset of AS

for q, a, b, c, a9, b9, c9 being Element of AS st q in A & q in P & q in C & q <> a & q <> b & q <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9 by Th49;

hence AS is Desarguesian by AFF_2:def 4; :: thesis: verum

assume AS is not AffinPlane ; :: thesis: AS is Desarguesian

then for A, P, C being Subset of AS

for q, a, b, c, a9, b9, c9 being Element of AS st q in A & q in P & q in C & q <> a & q <> b & q <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds

b,c // b9,c9 by Th49;

hence AS is Desarguesian by AFF_2:def 4; :: thesis: verum