let AS be AffinSpace; :: thesis: ( AS is not AffinPlane implies ProjHorizon AS is IncProjSp )
set XX = ProjHorizon AS;
A1: for a, b being Element of the Points of (ProjHorizon AS) ex A being Element of the Lines of (ProjHorizon AS) st
( a on A & b on A ) by Th40;
A2: for A being Element of the Lines of (ProjHorizon AS) ex a, b, c being Element of the Points of (ProjHorizon AS) st
( a <> b & b <> c & c <> a & a on A & b on A & c on A )

proof

let A be Element of the Lines of (ProjHorizon AS); :: thesis: ex a, b, c being Element of the Points of (ProjHorizon AS) st
( a <> b & b <> c & c <> a & a on A & b on A & c on A )
consider a, b, c being Element of the Points of (ProjHorizon AS) such that
A3: a on A and
A4: b on A and
A5: c on A and
A6: a <> b and
A7: b <> c and
A8: c <> a by Th39;
take a ; :: thesis: ex b, c being Element of the Points of (ProjHorizon AS) st
( a <> b & b <> c & c <> a & a on A & b on A & c on A )
take b ; :: thesis: ex c being Element of the Points of (ProjHorizon AS) st
( a <> b & b <> c & c <> a & a on A & b on A & c on A )
take c ; :: thesis: ( a <> b & b <> c & c <> a & a on A & b on A & c on A )
thus ( a <> b & b <> c & c <> a & a on A & b on A & c on A ) by A3, A4, A5, A6, A7, A8; :: thesis: verum

end;

assume AS is not AffinPlane ; :: thesis: ProjHorizon AS is IncProjSp
then A9: not for a being Element of the Points of (ProjHorizon AS)
for A being Element of the Lines of (ProjHorizon AS) holds a on A by Lm1;
A10: for a, b, c, d, p, q being Element of the Points of (ProjHorizon AS)
for M, N, P, Q being Element of the Lines of (ProjHorizon AS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N holds
ex q being Element of the Points of (ProjHorizon AS) st
( q on P & q on Q ) by Th44;
for a, b being Element of the Points of (ProjHorizon AS)
for A, K being Element of the Lines of (ProjHorizon AS) st a on A & b on A & a on K & b on K & not a = b holds
A = K by Th38;
hence ProjHorizon AS is IncProjSp by A1, A9, A2, A10, INCPROJ:def 4, INCPROJ:def 5, INCPROJ:def 6, INCPROJ:def 7, INCPROJ:def 8; :: thesis: verum