set L = { B where B is Subset of X : card B = k + 1 } ;
set P = { A where A is Subset of X : card A = k } ;
set I = (RelIncl (bool X)) /\ [: { A where A is Subset of X : card A = k } , { B where B is Subset of X : card B = k + 1 } :];
consider B being set such that
A3: ( B c= X & card B = k + 1 ) by ;
B in { B where B is Subset of X : card B = k + 1 } by A3;
then reconsider L = { B where B is Subset of X : card B = k + 1 } as non empty set ;
k <= k + 1 by NAT_1:11;
then Segm k c= Segm (k + 1) by NAT_1:39;
then k c= card X by A2;
then consider A being set such that
A4: ( A c= X & card A = k ) by CARD_FIL:36;
A in { A where A is Subset of X : card A = k } by A4;
then reconsider P = { A where A is Subset of X : card A = k } as non empty set ;
reconsider I = (RelIncl (bool X)) /\ [: { A where A is Subset of X : card A = k } , { B where B is Subset of X : card B = k + 1 } :] as Relation of P,L by XBOOLE_1:17;
set G = IncProjStr(# P,L,I #);
A5: IncProjStr(# P,L,I #) is up-2-rank
proof
let a, b be POINT of IncProjStr(# P,L,I #); :: according to INCSP_1:def 10 :: thesis: for b1, b2 being Element of the Lines of IncProjStr(# P,L,I #) holds
( a = b or not {a,b} on b1 or not {a,b} on b2 or b1 = b2 )

let l1, l2 be LINE of IncProjStr(# P,L,I #); :: thesis: ( a = b or not {a,b} on l1 or not {a,b} on l2 or l1 = l2 )
assume that
A6: a <> b and
A7: {a,b} on l1 and
A8: {a,b} on l2 ; :: thesis: l1 = l2
b in P ;
then A9: ex B being Subset of X st
( b = B & card B = k ) ;
a in P ;
then A10: ex A being Subset of X st
( a = A & card A = k ) ;
then A11: k + 1 c= card (a \/ b) by A9, A6, Th1;
l1 in L ;
then A12: ex C being Subset of X st
( l1 = C & card C = k + 1 ) ;
then A13: l1 is finite ;
A14: b in {a,b} by TARSKI:def 2;
then b on l1 by A7;
then [b,l1] in I ;
then [b,l1] in RelIncl (bool X) by XBOOLE_0:def 4;
then A15: b c= l1 by ;
l2 in L ;
then A16: ex D being Subset of X st
( l2 = D & card D = k + 1 ) ;
then A17: l2 is finite ;
A18: a in {a,b} by TARSKI:def 2;
then a on l2 by A8;
then [a,l2] in I ;
then [a,l2] in RelIncl (bool X) by XBOOLE_0:def 4;
then A19: a c= l2 by ;
b on l2 by ;
then [b,l2] in I ;
then [b,l2] in RelIncl (bool X) by XBOOLE_0:def 4;
then A20: b c= l2 by ;
then a \/ b c= l2 by ;
then card (a \/ b) c= k + 1 by ;
then A21: card (a \/ b) = k + 1 by ;
a on l1 by ;
then [a,l1] in I ;
then [a,l1] in RelIncl (bool X) by XBOOLE_0:def 4;
then a c= l1 by ;
then a \/ b = l1 by ;
hence l1 = l2 by ; :: thesis: verum
end;
IncProjStr(# P,L,I #) is with_non-trivial_lines
proof
let l be LINE of IncProjStr(# P,L,I #); :: according to INCSP_1:def 8 :: thesis: ex b1, b2 being Element of the Points of IncProjStr(# P,L,I #) st
( not b1 = b2 & {b1,b2} on l )

l in L ;
then consider C being Subset of X such that
A22: l = C and
A23: card C = k + 1 ;
1 < k + 1 by ;
then 1 + 1 <= k + 1 by NAT_1:13;
then Segm 2 c= Segm (k + 1) by NAT_1:39;
then consider a, b being object such that
A24: a in C and
A25: b in C and
A26: a <> b by ;
reconsider x = C \ {a}, y = C \ {b} as Subset of X ;
card x = k by ;
then A27: x in P ;
card y = k by ;
then y in P ;
then reconsider x = x, y = y as POINT of IncProjStr(# P,L,I #) by A27;
take x ; :: thesis: ex b1 being Element of the Points of IncProjStr(# P,L,I #) st
( not x = b1 & {x,b1} on l )

take y ; :: thesis: ( not x = y & {x,y} on l )
not b in {a} by ;
then ( b in {b} & b in x ) by ;
hence x <> y by XBOOLE_0:def 5; :: thesis: {x,y} on l
A28: ( C c= {a} \/ C & C c= {b} \/ C ) by XBOOLE_1:7;
{x,y} on l
proof
let z be POINT of IncProjStr(# P,L,I #); :: according to INCSP_1:def 4 :: thesis: ( not z in {x,y} or z on l )
assume z in {x,y} ; :: thesis: z on l
then A29: ( z = x or z = y ) by TARSKI:def 2;
then z c= l by ;
then [z,l] in RelIncl (bool X) by ;
then [z,l] in I by XBOOLE_0:def 4;
hence z on l ; :: thesis: verum
end;
hence {x,y} on l ; :: thesis: verum
end;
hence ex b1 being strict PartialLinearSpace st
( the Points of b1 = { A where A is Subset of X : card A = k } & the Lines of b1 = { L where L is Subset of X : card L = k + 1 } & the Inc of b1 = (RelIncl (bool X)) /\ [: the Points of b1, the Lines of b1:] ) by A5; :: thesis: verum