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 #); ( 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 )
INCSP_1:def 8 ( IT is linear & IT is up-2-rank & IT is strict )
thus
IT is linear
( IT is up-2-rank & IT is strict )
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
INCSP_1:def 10 IT is strict proof
let A,
B be
POINT of
IT;
for K, L being LINE of IT st A <> B & {A,B} on K & {A,B} on L holds
K = Llet K,
L be
LINE of
IT;
( 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 )
;
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;
verum
end;
thus
IT is strict
; verum