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 )
proof
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;
thus IT is linear :: thesis: ( IT is up-2-rank & IT is strict )
proof
let A, B be POINT of IT; :: according to INCPROJ:def 5 :: thesis: ex b1 being Element of the Lines of IT st
( A on b1 & B on b1 )
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;
thus for A, B being POINT of IT
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
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;
thus IT is strict ; :: thesis: verum