let AS be AffinSpace; :: thesis: ( AS is not AffinPlane implies ProjHorizon AS is IncProjSp )
assume A1: AS is not AffinPlane ; :: thesis: ProjHorizon AS is IncProjSp
set XX = ProjHorizon AS;
A2: 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;
A3: 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;
A4: 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 A1, Lm1;
A5: 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
A6: ( a on A & b on A & c on A & a <> b & b <> c & 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 A6; :: thesis: verum

end;

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;
hence ProjHorizon AS is IncProjSp by A2, A3, A4, A5, INCPROJ:def 9, INCPROJ:def 10, INCPROJ:def 11, INCPROJ:def 12, INCPROJ:def 13; :: thesis: verum