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
A1:
( B c= X & card B = k + 1 )
by B2, CARD_FIL:36;
B in { B where B is Subset of X : card B = k + 1 }
by A1;
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
k c= k + 1
by NAT_1:39;
then
k c= card X
by B2, 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 ;
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 #);
A3:
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 A4:
a <> b
and A5:
{a,b} on l1
and A6:
{a,b} on l2
;
l1 = l2
b in P
;
then A7:
ex
B being
Subset of
X st
(
b = B &
card B = k )
;
a in P
;
then A8:
ex
A being
Subset of
X st
(
a = A &
card A = k )
;
then A9:
k + 1
c= card (a \/ b)
by A7, A4, Th1;
l1 in L
;
then A10:
ex
C being
Subset of
X st
(
l1 = C &
card C = k + 1 )
;
then A11:
l1 is
finite
;
A12:
b in {a,b}
by TARSKI:def 2;
then
b on l1
by A5, INCSP_1:def 4;
then
[b,l1] in I
by INCSP_1:def 1;
then
[b,l1] in RelIncl (bool X)
by XBOOLE_0:def 4;
then A13:
b c= l1
by A7, A10, WELLORD2:def 1;
l2 in L
;
then A14:
ex
D being
Subset of
X st
(
l2 = D &
card D = k + 1 )
;
then A15:
l2 is
finite
;
A16:
a in {a,b}
by TARSKI:def 2;
then
a on l2
by A6, INCSP_1:def 4;
then
[a,l2] in I
by INCSP_1:def 1;
then
[a,l2] in RelIncl (bool X)
by XBOOLE_0:def 4;
then A17:
a c= l2
by A8, A14, WELLORD2:def 1;
b on l2
by A12, A6, INCSP_1:def 4;
then
[b,l2] in I
by INCSP_1:def 1;
then
[b,l2] in RelIncl (bool X)
by XBOOLE_0:def 4;
then A18:
b c= l2
by A7, A14, WELLORD2:def 1;
then
a \/ b c= l2
by A17, XBOOLE_1:8;
then
card (a \/ b) c= k + 1
by A14, CARD_1:11;
then A19:
card (a \/ b) = k + 1
by A9, XBOOLE_0:def 10;
a on l1
by A16, A5, INCSP_1:def 4;
then
[a,l1] in I
by INCSP_1:def 1;
then
[a,l1] in RelIncl (bool X)
by XBOOLE_0:def 4;
then
a c= l1
by A8, A10, WELLORD2:def 1;
then
a \/ b = l1
by A10, A13, A19, A11, CARD_FIN:1, XBOOLE_1:8;
hence
l1 = l2
by A14, A17, A18, A19, A15, CARD_FIN:1, 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 A20:
l = C
and A21:
card C = k + 1
;
1
< k + 1
by B1, XREAL_1:29;
then
1
+ 1
<= k + 1
by NAT_1:13;
then
2
c= k + 1
by NAT_1:39;
then consider a,
b being
set such that A22:
a in C
and A23:
b in C
and A24:
a <> b
by A21, PENCIL_1:2;
reconsider x =
C \ {a},
y =
C \ {b} as
Subset of
X ;
card x = k
by A21, A22, STIRL2_1:55;
then A25:
x in P
;
card y = k
by A21, A23, STIRL2_1:55;
then
y in P
;
then reconsider x =
x,
y =
y as
POINT of
IncProjStr(#
P,
L,
I #)
by A25;
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 A24, TARSKI:def 1;
then
(
b in {b} &
b in x )
by A23, TARSKI:def 1, XBOOLE_0:def 5;
hence
x <> y
by XBOOLE_0:def 5;
{x,y} on l
A26:
(
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 A27:
(
z = x or
z = y )
by TARSKI:def 2;
then
z c= l
by A20, A26, XBOOLE_1:43;
then
[z,l] in RelIncl (bool X)
by A20, A27, WELLORD2:def 1;
then
[z,l] in I
by XBOOLE_0:def 4;
hence
z on l
by INCSP_1:def 1;
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 A3; verum