set P = { A where A is Subset of X : card A = k } ;
set L = { B where B is Subset of X : card B = k + 1 } ;
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 } :];
k <= k + 1 by NAT_1:11;
then ( k c= k + 1 & k + 1 c= card X ) by A1, NAT_1:40;
then k c= card X by XBOOLE_1:1;
then consider A being set such that
A2: ( A c= X & card A = k ) by CARD_FIL:36;
A in { A where A is Subset of X : card A = k } by A2;
then reconsider P = { A where A is Subset of X : card A = k } as non empty set ;
consider B being set such that
A3: ( B c= X & card B = k + 1 ) by A1, CARD_FIL:36;
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 ;
(RelIncl (bool X)) /\ [:{ A where A is Subset of X : card A = k } ,{ B where B is Subset of X : card B = k + 1 } :] c= [:P,L:] by XBOOLE_1:17;
then 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 ;
set G = IncProjStr(# P,L,I #);
A4: 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 b₁, b₂ being Element of the Points of IncProjStr(# P,L,I #) st
( not b₁ = b₂ & {b₁,b₂} on l )
l in L ;
then consider C being Subset of X such that
A5: ( l = C & card C = k + 1 ) ;
1 < k + 1 by A1, XREAL_1:31;
then 1 + 1 <= k + 1 by NAT_1:13;
then 2 c= k + 1 by NAT_1:40;
then consider a, b being set such that
A6: ( a in C & b in C & a <> b ) by A5, PENCIL_1:2;
A7: ( C c= {a} \/ C & C c= {b} \/ C ) by XBOOLE_1:7;
reconsider x = C \ {a}, y = C \ {b} as Subset of X ;
( card x = k & card y = k ) by A5, A6, STIRL2_1:65;
then ( x in P & y in P ) ;
then reconsider x = x, y = y as POINT of IncProjStr(# P,L,I #) ;
take x ; :: thesis: ex b₁ being Element of the Points of IncProjStr(# P,L,I #) st
( not x = b₁ & {x,b₁} on l )
take y ; :: thesis: ( not x = y & {x,y} on l )
thus x <> y :: thesis: {x,y} on l

proof

A8: b in {b} by TARSKI:def 1;
not b in {a} by A6, TARSKI:def 1;
then ( b in x & not b in y ) by A6, A8, XBOOLE_0:def 5;
hence x <> y ; :: thesis: verum

end;

{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 ( z = x or z = y ) by TARSKI:def 2;
then ( z in bool X & z c= l ) by A5, A7, XBOOLE_1:43;
then [z,l] in RelIncl (bool X) by A5, WELLORD2:def 1;
then [z,l] in I by XBOOLE_0:def 4;
hence z on l by INCSP_1:def 1; :: thesis: verum

end;

hence {x,y} on l ; :: thesis: verum

end;

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 b₁, b₂ being Element of the Lines of IncProjStr(# P,L,I #) holds
( a = b or not {a,b} on b₁ or not {a,b} on b₂ or b₁ = b₂ )
a in P ;
then consider A being Subset of X such that
A9: ( a = A & card A = k ) ;
b in P ;
then consider B being Subset of X such that
A10: ( b = B & card B = k ) ;
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 )
l1 in L ;
then consider C being Subset of X such that
A11: ( l1 = C & card C = k + 1 ) ;
l2 in L ;
then consider D being Subset of X such that
A12: ( l2 = D & card D = k + 1 ) ;
A13: ( a in {a,b} & b in {a,b} ) by TARSKI:def 2;
assume A14: ( a <> b & {a,b} on l1 & {a,b} on l2 ) ; :: thesis: l1 = l2
then ( a on l1 & b on l1 & a on l2 & b on l2 ) by A13, INCSP_1:def 4;
then ( [a,l1] in I & [b,l1] in I & [a,l2] in I & [b,l2] in I ) by INCSP_1:def 1;
then ( [a,l1] in RelIncl (bool X) & [b,l1] in RelIncl (bool X) & [a,l2] in RelIncl (bool X) & [b,l2] in RelIncl (bool X) ) by XBOOLE_0:def 4;
then A15: ( a c= l1 & b c= l1 & a c= l2 & b c= l2 ) by A9, A10, A11, A12, WELLORD2:def 1;
then ( a \/ b c= l1 & a \/ b c= l2 ) by XBOOLE_1:8;
then A16: card (a \/ b) c= k + 1 by A12, CARD_1:27;
k + 1 c= card (a \/ b) by A9, A10, A14, Th1;
then A17: ( card (a \/ b) = k + 1 & card (k + 1) = k + 1 ) by A16, CARD_1:def 5, XBOOLE_0:def 10;
then ( a \/ b is finite & l2 is finite & l1 is finite ) by A11, A12;
then ( a \/ b = l1 & a \/ b = l2 ) by A11, A12, A15, A17, CARD_FIN:1, XBOOLE_1:8;
hence l1 = l2 ; :: thesis: verum

end;

hence ex b₁ being strict PartialLinearSpace st
( the Points of b₁ = { A where A is Subset of X : card A = k } & the Lines of b₁ = { L where L is Subset of X : card L = k + 1 } & the Inc of b₁ = (RelIncl (bool X)) /\ [:the Points of b₁,the Lines of b₁:] ) by A4; :: thesis: verum