let AS be AffinSpace; ( 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);
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
;
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
;
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
;
( 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;
verum
end;
assume
AS is not AffinPlane
; 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; verum