set P = the strict IncSpace-like IncStruct ;

take IT = IncProjStr(# the Points of the strict IncSpace-like IncStruct , the Lines of the strict IncSpace-like IncStruct , the Inc of the strict IncSpace-like IncStruct #); :: thesis: ( IT is with_non-trivial_lines & IT is linear & IT is up-2-rank & IT is strict )

thus for L being LINE of IT ex A, B being POINT of IT 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 )

for K, L being LINE of IT st A <> B & {A,B} on K & {A,B} on L holds

K = L :: according to INCSP_1:def 10 :: thesis: IT is strict

take IT = IncProjStr(# the Points of the strict IncSpace-like IncStruct , the Lines of the strict IncSpace-like IncStruct , the Inc of the strict IncSpace-like IncStruct #); :: thesis: ( IT is with_non-trivial_lines & IT is linear & IT is up-2-rank & IT is strict )

thus for L being LINE of IT ex A, B being POINT of IT 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

thus
IT is linear
:: thesis: ( IT is up-2-rank & IT is strict )
let L be LINE of IT; :: thesis: ex A, B being POINT of IT st

( A <> B & {A,B} on L )

reconsider L9 = L as LINE of the strict IncSpace-like IncStruct ;

consider A9, B9 being POINT of the strict IncSpace-like IncStruct such that

A1: ( A9 <> B9 & {A9,B9} on L9 ) by INCSP_1:def 8;

reconsider A = A9, B = B9 as POINT of IT ;

take A ; :: thesis: ex B being POINT of IT 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;( A <> B & {A,B} on L )

reconsider L9 = L as LINE of the strict IncSpace-like IncStruct ;

consider A9, B9 being POINT of the strict IncSpace-like IncStruct such that

A1: ( A9 <> B9 & {A9,B9} on L9 ) by INCSP_1:def 8;

reconsider A = A9, B = B9 as POINT of IT ;

take A ; :: thesis: ex B being POINT of IT 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

proof

thus
for A, B being POINT of IT
let A, B be POINT of IT; :: according to INCPROJ:def 5 :: thesis: ex b_{1} being Element of the Lines of IT st

( A on b_{1} & B on b_{1} )

reconsider A9 = A, B9 = B as POINT of the strict IncSpace-like IncStruct ;

consider L9 being LINE of the strict IncSpace-like IncStruct such that

A2: {A9,B9} on L9 by INCSP_1:def 9;

reconsider L = L9 as LINE of IT ;

take L ; :: thesis: ( A on L & B on L )

( A9 on L9 & B9 on L9 ) by A2, INCSP_1:1;

hence ( A on L & B on L ) ; :: thesis: verum

end;( A on b

reconsider A9 = A, B9 = B as POINT of the strict IncSpace-like IncStruct ;

consider L9 being LINE of the strict IncSpace-like IncStruct such that

A2: {A9,B9} on L9 by INCSP_1:def 9;

reconsider L = L9 as LINE of IT ;

take L ; :: thesis: ( A on L & B on L )

( A9 on L9 & B9 on L9 ) by A2, INCSP_1:1;

hence ( A on L & B on L ) ; :: thesis: verum

for K, L being LINE of IT 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

thus
IT is strict
; :: thesis: verum
let A, B be POINT of IT; :: thesis: for K, L being LINE of IT st A <> B & {A,B} on K & {A,B} on L holds

K = L

let K, L be LINE of IT; :: 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 K9 = K, L9 = L as LINE of the strict IncSpace-like IncStruct ;

reconsider A9 = A, B9 = B as POINT of the strict IncSpace-like IncStruct ;

( {A9,B9} on K9 & {A9,B9} on L9 ) by A4, Th9;

hence K = L by A3, INCSP_1:def 10; :: thesis: verum

end;K = L

let K, L be LINE of IT; :: 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 K9 = K, L9 = L as LINE of the strict IncSpace-like IncStruct ;

reconsider A9 = A, B9 = B as POINT of the strict IncSpace-like IncStruct ;

( {A9,B9} on K9 & {A9,B9} on L9 ) by A4, Th9;

hence K = L by A3, INCSP_1:def 10; :: thesis: verum