set XX = IncProjSp_of AS;
A1: for a, b being POINT of (IncProjSp_of AS) ex A being LINE of (IncProjSp_of AS) st
( a on A & b on A ) by Lm4;
A2: not for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) holds a on A by Lm6;
A3: for A being LINE of (IncProjSp_of AS) ex a, b, c being POINT of (IncProjSp_of AS) st
( a <> b & b <> c & c <> a & a on A & b on A & c on A )

proof

let A be LINE of (IncProjSp_of AS); :: thesis: ex a, b, c being POINT of (IncProjSp_of AS) st
( a <> b & b <> c & c <> a & a on A & b on A & c on A )
consider a, b, c being POINT of (IncProjSp_of AS) such that
A4: a on A and
A5: b on A and
A6: c on A and
A7: a <> b and
A8: b <> c and
A9: c <> a by Lm3;
take a ; :: thesis: ex b, c being POINT of (IncProjSp_of AS) st
( a <> b & b <> c & c <> a & a on A & b on A & c on A )
take b ; :: thesis: ex c being POINT of (IncProjSp_of 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 A4, A5, A6, A7, A8, A9; :: thesis: verum

end;

A10: for a, b, c, d, p, q being POINT of (IncProjSp_of AS)
for M, N, P, Q being LINE of (IncProjSp_of 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 POINT of (IncProjSp_of AS) st
( q on P & q on Q ) by Lm12;
for a, b being POINT of (IncProjSp_of AS)
for A, K being LINE of (IncProjSp_of AS) st a on A & b on A & a on K & b on K & not a = b holds
A = K by Lm2;
hence ( IncProjSp_of AS is partial & IncProjSp_of AS is linear & IncProjSp_of AS is up-2-dimensional & IncProjSp_of AS is up-3-rank & IncProjSp_of AS is Vebleian ) by A1, A2, A3, A10, INCPROJ:def 4, INCPROJ:def 5, INCPROJ:def 6, INCPROJ:def 7, INCPROJ:def 8; :: thesis: verum