let AS be AffinSpace; ( IncProjSp_of AS is 2-dimensional implies AS is AffinPlane )
set x = the Element of AS;
assume A1:
IncProjSp_of AS is 2-dimensional
; AS is AffinPlane
consider X being Subset of AS such that
A2:
the Element of AS in X
and
the Element of AS in X
and
the Element of AS in X
and
A3:
X is being_plane
by AFF_4:37;
assume
AS is not AffinPlane
; contradiction
then consider z being Element of AS such that
A4:
not z in X
by A3, AFF_4:48;
set Y = Line ( the Element of AS,z);
A5:
Line ( the Element of AS,z) is being_line
by A2, A4, AFF_1:def 3;
then reconsider A = [(PDir X),2], K = [(Line ( the Element of AS,z)),1] as LINE of (IncProjSp_of AS) by A3, Th23;
consider a being POINT of (IncProjSp_of AS) such that
A6:
a on A
and
A7:
a on K
by A1, INCPROJ:def 9;
a is not Element of AS
by A6, Th27;
then consider Y9 being Subset of AS such that
A8:
a = LDir Y9
and
A9:
Y9 is being_line
by Th20;
Y9 '||' Line ( the Element of AS,z)
by A5, A7, A8, A9, Th28;
then A10:
Y9 // Line ( the Element of AS,z)
by A5, A9, AFF_4:40;
A11:
z in Line ( the Element of AS,z)
by AFF_1:15;
A12:
the Element of AS in Line ( the Element of AS,z)
by AFF_1:15;
Y9 '||' X
by A3, A6, A8, A9, Th29;
then
Line ( the Element of AS,z) c= X
by A2, A3, A5, A12, A10, AFF_4:43, AFF_4:56;
hence
contradiction
by A4, A11; verum