consider P being strict IncSpace-like IncStruct ;
take IT = IncProjStr(# the Points of P,the Lines of P,the Inc of P #); :: thesis: ( IT is with_non-trivial_lines & IT is linear & IT is up-2-rank & IT is strict )
thus for L being LINE of ex A, B being POINT of st
( A <> B & {A,B} on L ) :: according to INCSP_1:def 8 :: thesis: ( IT is linear & IT is up-2-rank & IT is strict )

proof

let L be LINE of ; :: thesis: ex A, B being POINT of st
( A <> B & {A,B} on L )
reconsider L' = L as LINE of ;
consider A', B' being POINT of such that
A1: ( A' <> B' & {A',B'} on L' ) by INCSP_1:def 8;
reconsider A = A', B = B' as POINT of ;
take A ; :: thesis: ex B being POINT of st
( A <> B & {A,B} on L )
take B ; :: thesis: ( A <> B & {A,B} on L )
thus ( A <> B & {A,B} on L ) by A1, Th9; :: thesis: verum

end;

thus IT is linear :: thesis: ( IT is up-2-rank & IT is strict )

proof

let A, B be POINT of ; :: according to INCPROJ:def 10 :: thesis: ex b₁ being Element of the Lines of IT st
( A on b₁ & B on b₁ )
reconsider A' = A, B' = B as POINT of ;
consider L' being LINE of such that
A2: {A',B'} on L' by INCSP_1:def 9;
reconsider L = L' as LINE of ;
take L ; :: thesis: ( A on L & B on L )
( A' on L' & B' on L' ) by A2, INCSP_1:11;
hence ( A on L & B on L ) by Th8; :: thesis: verum

end;

thus for A, B being POINT of
for K, L being LINE of st A <> B & {A,B} on K & {A,B} on L holds
K = L :: according to INCSP_1:def 10 :: thesis: IT is strict

proof

let A, B be POINT of ; :: thesis: for K, L being LINE of st A <> B & {A,B} on K & {A,B} on L holds
K = L
let K, L be LINE of ; :: thesis: ( A <> B & {A,B} on K & {A,B} on L implies K = L )
assume that
A3: A <> B and
A4: ( {A,B} on K & {A,B} on L ) ; :: thesis: K = L
reconsider K' = K, L' = L as LINE of ;
reconsider A' = A, B' = B as POINT of ;
( {A',B'} on K' & {A',B'} on L' ) by A4, Th9;
hence K = L by A3, INCSP_1:def 10; :: thesis: verum

end;

thus IT is strict ; :: thesis: verum