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
proof
let a,
b be
POINT of
IncProjStr(#
P,
L,
I #);
INCSP_1:def 10 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 #);
( 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
;
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;
verum
end;
IncProjStr(# P,L,I #) is with_non-trivial_lines
proof
let l be
LINE of
IncProjStr(#
P,
L,
I #);
INCSP_1:def 8 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 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
;
ex b1 being Element of the Points of IncProjStr(# P,L,I #) st
( not x = b1 & {x,b1} on l )
take
y
;
( 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;
{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 #);
INCSP_1:def 4 ( not z in {x,y} or z on l )
assume
z in {x,y}
;
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
;
verum
end;
hence
{x,y} on l
;
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; verum