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 A2, 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 ;

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_{1} being strict PartialLinearSpace st

( the Points of b_{1} = { A where A is Subset of X : card A = k } & the Lines of b_{1} = { L where L is Subset of X : card L = k + 1 } & the Inc of b_{1} = (RelIncl (bool X)) /\ [: the Points of b_{1}, the Lines of b_{1}:] )
by A5; :: thesis: verum

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 A2, 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 ;

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

IncProjStr(# P,L,I #) is with_non-trivial_lines
let a, b be POINT of IncProjStr(# P,L,I #); :: according to INCSP_1:def 10 :: thesis: for b_{1}, b_{2} being Element of the Lines of IncProjStr(# P,L,I #) holds

( a = b or not {a,b} on b_{1} or not {a,b} on b_{2} or b_{1} = b_{2} )

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 A9, A12, WELLORD2:def 1;

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 A10, A16, WELLORD2:def 1;

b on l2 by A14, A8;

then [b,l2] in I ;

then [b,l2] in RelIncl (bool X) by XBOOLE_0:def 4;

then A20: b c= l2 by A9, A16, WELLORD2:def 1;

then a \/ b c= l2 by A19, XBOOLE_1:8;

then card (a \/ b) c= k + 1 by A16, CARD_1:11;

then A21: card (a \/ b) = k + 1 by A11, XBOOLE_0:def 10;

a on l1 by A18, A7;

then [a,l1] in I ;

then [a,l1] in RelIncl (bool X) by XBOOLE_0:def 4;

then a c= l1 by A10, A12, WELLORD2:def 1;

then a \/ b = l1 by A12, A15, A21, A13, CARD_2:102, XBOOLE_1:8;

hence l1 = l2 by A16, A19, A20, A21, A17, CARD_2:102, XBOOLE_1:8; :: thesis: verum

end;( a = b or not {a,b} on b

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 A9, A12, WELLORD2:def 1;

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 A10, A16, WELLORD2:def 1;

b on l2 by A14, A8;

then [b,l2] in I ;

then [b,l2] in RelIncl (bool X) by XBOOLE_0:def 4;

then A20: b c= l2 by A9, A16, WELLORD2:def 1;

then a \/ b c= l2 by A19, XBOOLE_1:8;

then card (a \/ b) c= k + 1 by A16, CARD_1:11;

then A21: card (a \/ b) = k + 1 by A11, XBOOLE_0:def 10;

a on l1 by A18, A7;

then [a,l1] in I ;

then [a,l1] in RelIncl (bool X) by XBOOLE_0:def 4;

then a c= l1 by A10, A12, WELLORD2:def 1;

then a \/ b = l1 by A12, A15, A21, A13, CARD_2:102, XBOOLE_1:8;

hence l1 = l2 by A16, A19, A20, A21, A17, CARD_2:102, XBOOLE_1:8; :: thesis: verum

proof

hence
ex b
let l be LINE of IncProjStr(# P,L,I #); :: according to INCSP_1:def 8 :: thesis: ex b_{1}, b_{2} being Element of the Points of IncProjStr(# P,L,I #) st

( not b_{1} = b_{2} & {b_{1},b_{2}} 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 A1, XREAL_1:29;

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 A23, PENCIL_1:2;

reconsider x = C \ {a}, y = C \ {b} as Subset of X ;

card x = k by A23, A24, STIRL2_1:55;

then A27: x in P ;

card y = k by A23, A25, STIRL2_1:55;

then y in P ;

then reconsider x = x, y = y as POINT of IncProjStr(# P,L,I #) by A27;

take x ; :: thesis: ex b_{1} being Element of the Points of IncProjStr(# P,L,I #) st

( not x = b_{1} & {x,b_{1}} on l )

take y ; :: thesis: ( not x = y & {x,y} on l )

not b in {a} by A26, TARSKI:def 1;

then ( b in {b} & b in x ) by A25, TARSKI:def 1, XBOOLE_0:def 5;

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

end;( not b

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 A1, XREAL_1:29;

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 A23, PENCIL_1:2;

reconsider x = C \ {a}, y = C \ {b} as Subset of X ;

card x = k by A23, A24, STIRL2_1:55;

then A27: x in P ;

card y = k by A23, A25, STIRL2_1:55;

then y in P ;

then reconsider x = x, y = y as POINT of IncProjStr(# P,L,I #) by A27;

take x ; :: thesis: ex b

( not x = b

take y ; :: thesis: ( not x = y & {x,y} on l )

not b in {a} by A26, TARSKI:def 1;

then ( b in {b} & b in x ) by A25, TARSKI:def 1, XBOOLE_0:def 5;

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

hence
{x,y} on l
; :: thesis: verum
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 A22, A28, XBOOLE_1:43;

then [z,l] in RelIncl (bool X) by A22, A29, WELLORD2:def 1;

then [z,l] in I by XBOOLE_0:def 4;

hence z on l ; :: thesis: verum

end;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 A22, A28, XBOOLE_1:43;

then [z,l] in RelIncl (bool X) by A22, A29, WELLORD2:def 1;

then [z,l] in I by XBOOLE_0:def 4;

hence z on l ; :: thesis: verum

( the Points of b