let k be Element of NAT ; :: thesis:
let X be non empty set ; :: thesis:
assume that
A1: 0 < k and
A2: k + 1 c= card X ; :: thesis:
let o, b1, a1, b2, a2, b3, a3, r, s, t be POINT of (G_ (k,X)); :: according to INCPROJ:def 13 :: thesis:
let C1, C2, C3, A1, A2, A3, B1, B2, B3 be LINE of (G_ (k,X)); :: thesis:
assume that
A3: {o,b1,a1} on C1 and
A4: {o,a2,b2} on C2 and
A5: {o,a3,b3} on C3 and
A6: {a3,a2,t} on A1 and
A7: {a3,r,a1} on A2 and
A8: {a2,s,a1} on A3 and
A9: {t,b2,b3} on B1 and
A10: {b1,r,b3} on B2 and
A11: {b1,s,b2} on B3 and
A12: C1,C2,C3 are_mutually_distinct and
A13: o <> a1 and
A14: ( o <> a2 & o <> a3 ) and
A15: o <> b1 and
A16: ( o <> b2 & o <> b3 ) and
A17: a1 <> b1 and
A18: a2 <> b2 and
A19: a3 <> b3 ; :: thesis:
A20: o on C1 by A3, INCSP_1:2;
A21: b2 on C2 by A4, INCSP_1:2;
then A22: b2 c= C2 by A1, A2, Th10;
A23: a2 on C2 by A4, INCSP_1:2;
then A24: {a2,b2} on C2 by A21, INCSP_1:1;
A25: o on C2 by A4, INCSP_1:2;
then A26: {o,b2} on C2 by A21, INCSP_1:1;
A27: {o,a2} on C2 by A25, A23, INCSP_1:1;
A28: ( a3 on A1 & a2 on A1 ) by A6, INCSP_1:2;
A29: b3 on B2 by A10, INCSP_1:2;
A30: b3 on C3 by A5, INCSP_1:2;
then A31: b3 c= C3 by A1, A2, Th10;
A32: a3 on C3 by A5, INCSP_1:2;
then A33: {a3,b3} on C3 by A30, INCSP_1:1;
A34: o on C3 by A5, INCSP_1:2;
then A35: {o,b3} on C3 by A30, INCSP_1:1;
A36: {o,a3} on C3 by A34, A32, INCSP_1:1;
A37: ( a3 on A2 & a1 on A2 ) by A7, INCSP_1:2;
A38: b1 on B3 by A11, INCSP_1:2;
A39: C1 <> C3 by A12, ZFMISC_1:def 5;
A40: b1 on B2 by A10, INCSP_1:2;
A41: C2 <> C3 by A12, ZFMISC_1:def 5;
A42: b3 on B1 by A9, INCSP_1:2;
A43: C1 <> C2 by A12, ZFMISC_1:def 5;
A44: b2 on B1 by A9, INCSP_1:2;
A45: a1 on C1 by A3, INCSP_1:2;
then A46: a1 c= C1 by A1, A2, Th10;
A47: b1 on C1 by A3, INCSP_1:2;
then A48: {o,b1} on C1 by A20, INCSP_1:1;
A49: b2 on B3 by A11, INCSP_1:2;
A50: {a1,b1} on C1 by A47, A45, INCSP_1:1;
A51: ( not a1 on B2 & not a2 on B3 & not a3 on B1 )

proof

assume ( a1 on B2 or a2 on B3 or a3 on B1 ) ; :: thesis:
then ( {a1,b1} on B2 or {a2,b2} on B3 or {a3,b3} on B1 ) by A42, A40, A49, INCSP_1:1;
then ( b3 on C1 or b1 on C2 or b2 on C3 ) by A17, A18, A19, A44, A29, A38, A50, A24, A33, INCSP_1:def 10;
then ( {o,b3} on C1 or {o,b1} on C2 or {o,b2} on C3 ) by A20, A25, A34, INCSP_1:1;
hence contradiction by A15, A16, A48, A26, A35, A43, A41, A39, INCSP_1:def 10; :: thesis:

end;

A52: ( s on A3 & s on B3 ) by A8, A11, INCSP_1:2;
A53: t on B1 by A9, INCSP_1:2;
A54: ( r on A2 & r on B2 ) by A7, A10, INCSP_1:2;
A55: t on A1 by A6, INCSP_1:2;
A56: a1 on A3 by A8, INCSP_1:2;
A57: a2 on A3 by A8, INCSP_1:2;
A58: the Lines of (G_ (k,X)) = { L where L is Subset of X : card L = k + 1 } by A1, A2, Def1;
A59: {o,a1} on C1 by A20, A45, INCSP_1:1;
A60: ( not o on A1 & not o on B1 & not o on A2 & not o on B2 & not o on A3 & not o on B3 )

proof

assume ( o on A1 or o on B1 or o on A2 or o on B2 or o on A3 or o on B3 ) ; :: thesis:
then ( ( {o,a2} on A1 & {o,a3} on A1 ) or ( {o,b2} on B1 & {o,b3} on B1 ) or ( {o,a1} on A2 & {o,a3} on A2 ) or ( {o,b1} on B2 & {o,b3} on B2 ) or ( {o,a2} on A3 & {o,a1} on A3 ) or ( {o,b2} on B3 & {o,b1} on B3 ) ) by A28, A37, A57, A56, A44, A42, A40, A29, A38, A49, INCSP_1:1;
then ( ( A1 = C2 & A1 = C3 ) or ( B1 = C2 & B1 = C3 ) or ( A2 = C1 & A2 = C3 ) or ( B2 = C1 & B2 = C3 ) or ( A3 = C2 & A3 = C1 ) or ( B3 = C2 & B3 = C1 ) ) by A13, A14, A15, A16, A59, A27, A36, A48, A26, A35, INCSP_1:def 10;
hence contradiction by A12, ZFMISC_1:def 5; :: thesis:

end;

then consider salpha being POINT of (G_ (k,X)) such that
A61: ( salpha on A3 & salpha on B3 ) and
A62: salpha = (a1 /\ b1) \/ (a2 /\ b2) by A1, A2, A20, A47, A45, A25, A23, A21, A57, A56, A38, A49, A43, A51, Th12;
consider ralpha being POINT of (G_ (k,X)) such that
A63: ( ralpha on B2 & ralpha on A2 ) and
A64: ralpha = (a1 /\ b1) \/ (a3 /\ b3) by A1, A2, A20, A47, A45, A34, A32, A30, A37, A40, A29, A39, A51, A60, Th12;
A65: ((a1 /\ b1) \/ (a3 /\ b3)) \/ (a2 /\ b2) = (a1 /\ b1) \/ ((a3 /\ b3) \/ (a2 /\ b2)) by XBOOLE_1:4;
consider talpha being POINT of (G_ (k,X)) such that
A66: ( talpha on A1 & talpha on B1 ) and
A67: talpha = (a2 /\ b2) \/ (a3 /\ b3) by A1, A2, A25, A23, A21, A34, A32, A30, A28, A44, A42, A41, A51, A60, Th12;
A68: ( A1 <> B1 & A2 <> B2 ) by A6, A7, A51, INCSP_1:2;
A69: ( r = ralpha & s = salpha & t = talpha )

proof

A70: ( {s,salpha} on A3 & {s,salpha} on B3 ) by A52, A61, INCSP_1:1;
A71: ( {r,ralpha} on A2 & {r,ralpha} on B2 ) by A54, A63, INCSP_1:1;
assume A72: ( r <> ralpha or s <> salpha or t <> talpha ) ; :: thesis:
( {t,talpha} on A1 & {t,talpha} on B1 ) by A55, A53, A66, INCSP_1:1;
hence contradiction by A57, A51, A68, A72, A71, A70, INCSP_1:def 10; :: thesis:

end;

then r \/ s = (((a3 /\ b3) \/ (a1 /\ b1)) \/ (a1 /\ b1)) \/ (a2 /\ b2) by A62, A64, XBOOLE_1:4;
then r \/ s = ((a3 /\ b3) \/ ((a1 /\ b1) \/ (a1 /\ b1))) \/ (a2 /\ b2) by XBOOLE_1:4;
then A73: (r \/ s) \/ t = ((a1 /\ b1) \/ (a3 /\ b3)) \/ (a2 /\ b2) by A67, A69, A65, XBOOLE_1:7, XBOOLE_1:12;
a2 c= C2 by A1, A2, A23, Th10;
then A74: a2 \/ b2 c= C2 by A22, XBOOLE_1:8;
r c= r \/ (s \/ t) by XBOOLE_1:7;
then A75: r c= (r \/ s) \/ t by XBOOLE_1:4;
C1 in the Lines of (G_ (k,X)) ;
then consider C11 being Subset of X such that
A76: ( C11 = C1 & card C11 = k + 1 ) by A58;
reconsider C1 = C1 as finite set by A76;
A77: b1 c= C1 by A1, A2, A47, Th10;
then a1 \/ b1 c= C1 by A46, XBOOLE_1:8;
then A78: card (a1 \/ b1) c= k + 1 by A76, CARD_1:11;
A79: the Points of (G_ (k,X)) = { A where A is Subset of X : card A = k } by A1, A2, Def1;
o in the Points of (G_ (k,X)) ;
then A80: ex o1 being Subset of X st
( o1 = o & card o1 = k ) by A79;
b1 in the Points of (G_ (k,X)) ;
then A81: ex b11 being Subset of X st
( b11 = b1 & card b11 = k ) by A79;
a3 in the Points of (G_ (k,X)) ;
then A82: ex a13 being Subset of X st
( a13 = a3 & card a13 = k ) by A79;
then A83: card a3 = (k - 1) + 1 ;
t in the Points of (G_ (k,X)) ;
then A84: ex t1 being Subset of X st
( t1 = t & card t1 = k ) by A79;
then A85: t is finite ;
a2 in the Points of (G_ (k,X)) ;
then A86: ex a12 being Subset of X st
( a12 = a2 & card a12 = k ) by A79;
then A87: card a2 = (k - 1) + 1 ;
s in the Points of (G_ (k,X)) ;
then A88: ex s1 being Subset of X st
( s1 = s & card s1 = k ) by A79;
then A89: s is finite ;
a1 in the Points of (G_ (k,X)) ;
then A90: ex a11 being Subset of X st
( a11 = a1 & card a11 = k ) by A79;
then k + 1 c= card (a1 \/ b1) by A81, A17, Th1;
then A91: card (a1 \/ b1) = (k - 1) + (2 * 1) by A78, XBOOLE_0:def 10;
A92: k - 1 is Element of NAT by A1, NAT_1:20;
C2 in the Lines of (G_ (k,X)) ;
then ex C12 being Subset of X st
( C12 = C2 & card C12 = k + 1 ) by A58;
then A93: card (a2 \/ b2) c= k + 1 by A74, CARD_1:11;
b2 in the Points of (G_ (k,X)) ;
then A94: ex b12 being Subset of X st
( b12 = b2 & card b12 = k ) by A79;
then k + 1 c= card (a2 \/ b2) by A86, A18, Th1;
then A95: card (a2 \/ b2) = (k - 1) + (2 * 1) by A93, XBOOLE_0:def 10;
then A96: card (a2 /\ b2) = k - 1 by A92, A94, A87, Th2;
A97: card (a2 /\ b2) = (k - 2) + 1 by A92, A94, A95, A87, Th2;
A98: card a1 = (k - 1) + 1 by A90;
then A99: card (a1 /\ b1) = k - 1 by A92, A81, A91, Th2;
a3 c= C3 by A1, A2, A32, Th10;
then A100: a3 \/ b3 c= C3 by A31, XBOOLE_1:8;
s c= s \/ (r \/ t) by XBOOLE_1:7;
then A101: s c= (r \/ s) \/ t by XBOOLE_1:4;
0 + 1 < k + 1 by A1, XREAL_1:8;
then 1 <= (k - 1) + 1 by NAT_1:13;
then ( 1 <= k - 1 or k = 1 ) by A92, NAT_1:8;
then A102: ( 1 + 1 <= (k - 1) + 1 or k = 1 ) by XREAL_1:6;
A103: o c= C1 by A1, A2, A20, Th10;
A104: not k = 1

proof

assume A105: k = 1 ; :: thesis:
then consider z1 being object such that
A106: o = {z1} by A80, CARD_2:42;
consider z3 being object such that
A107: b1 = {z3} by A81, A105, CARD_2:42;
consider z2 being object such that
A108: a1 = {z2} by A90, A105, CARD_2:42;
o \/ a1 c= C1 by A103, A46, XBOOLE_1:8;
then (o \/ a1) \/ b1 c= C1 by A77, XBOOLE_1:8;
then {z1,z2} \/ b1 c= C1 by A106, A108, ENUMSET1:1;
then A109: {z1,z2,z3} c= C1 by A107, ENUMSET1:3;
card {z1,z2,z3} = 3 by A13, A15, A17, A106, A108, A107, CARD_2:58;
then Segm 3 c= Segm (card C1) by A109, CARD_1:11;
hence contradiction by A76, A105, NAT_1:39; :: thesis:

end;

then A110: k - 2 is Element of NAT by A102, NAT_1:21;
C3 in the Lines of (G_ (k,X)) ;
then ex C13 being Subset of X st
( C13 = C3 & card C13 = k + 1 ) by A58;
then A111: card (a3 \/ b3) c= k + 1 by A100, CARD_1:11;
b3 in the Points of (G_ (k,X)) ;
then A112: ex b13 being Subset of X st
( b13 = b3 & card b13 = k ) by A79;
then k + 1 c= card (a3 \/ b3) by A82, A19, Th1;
then A113: card (a3 \/ b3) = (k - 1) + (2 * 1) by A111, XBOOLE_0:def 10;
then A114: card (a3 /\ b3) = k - 1 by A92, A112, A83, Th2;
r in the Points of (G_ (k,X)) ;
then A115: ex r1 being Subset of X st
( r1 = r & card r1 = k ) by A79;
then r \/ s c= X by A88, XBOOLE_1:8;
then A116: (r \/ s) \/ t c= X by A84, XBOOLE_1:8;
A117: card (a3 /\ b3) = (k - 2) + 1 by A92, A112, A113, A83, Th2;
A118: card (a1 /\ b1) = (k - 2) + 1 by A92, A81, A91, A98, Th2;
card ((a1 /\ b1) \/ (a2 /\ b2)) = (k - 2) + (2 * 1) by A62, A69, A88;
then A119: card ((a1 /\ b1) /\ (a2 /\ b2)) = k - 2 by A110, A118, A97, Th2;
card ((a2 /\ b2) \/ (a3 /\ b3)) = (k - 2) + (2 * 1) by A67, A69, A84;
then A120: card ((a2 /\ b2) /\ (a3 /\ b3)) = k - 2 by A110, A97, A117, Th2;
card ((a1 /\ b1) \/ (a3 /\ b3)) = (k - 2) + (2 * 1) by A64, A69, A115;
then A121: card ((a1 /\ b1) /\ (a3 /\ b3)) = k - 2 by A110, A118, A117, Th2;
A122: t c= (r \/ s) \/ t by XBOOLE_1:7;
A123: ( k = 2 implies ex O being LINE of (G_ (k,X)) st {r,s,t} on O )

proof

assume k = 2 ; :: thesis:
then card ((r \/ s) \/ t) = k + 1 by A99, A96, A114, A73, A121, A120, A119, Th7;
then (r \/ s) \/ t in the Lines of (G_ (k,X)) by A58, A116;
then consider O being LINE of (G_ (k,X)) such that
A124: O = (r \/ s) \/ t ;
A125: t on O by A1, A2, A122, A124, Th10;
( r on O & s on O ) by A1, A2, A75, A101, A124, Th10;
then {r,s,t} on O by A125, INCSP_1:2;
hence ex O being LINE of (G_ (k,X)) st {r,s,t} on O ; :: thesis:

end;

A126: r is finite by A115;
A127: ( 3 <= k implies ex O being LINE of (G_ (k,X)) st {r,s,t} on O )

proof

A128: ( card ((r \/ s) \/ t) = k + 1 implies ex O being LINE of (G_ (k,X)) st {r,s,t} on O )

proof

assume card ((r \/ s) \/ t) = k + 1 ; :: thesis:
then (r \/ s) \/ t in the Lines of (G_ (k,X)) by A58, A116;
then consider O being LINE of (G_ (k,X)) such that
A129: O = (r \/ s) \/ t ;
A130: t on O by A1, A2, A122, A129, Th10;
( r on O & s on O ) by A1, A2, A75, A101, A129, Th10;
then {r,s,t} on O by A130, INCSP_1:2;
hence ex O being LINE of (G_ (k,X)) st {r,s,t} on O ; :: thesis:

end;

A131: ( card ((r \/ s) \/ t) = k implies ex O being LINE of (G_ (k,X)) st {r,s,t} on O )

proof

assume A132: card ((r \/ s) \/ t) = k ; :: thesis:
then A133: t = (r \/ s) \/ t by A84, A126, A89, A85, CARD_2:102, XBOOLE_1:7;
( r = (r \/ s) \/ t & s = (r \/ s) \/ t ) by A115, A88, A126, A89, A85, A75, A101, A132, CARD_2:102;
then {r,s,t} on A1 by A55, A133, INCSP_1:2;
hence ex O being LINE of (G_ (k,X)) st {r,s,t} on O ; :: thesis:

end;

assume 3 <= k ; :: thesis:
hence ex O being LINE of (G_ (k,X)) st {r,s,t} on O by A99, A96, A114, A73, A102, A121, A120, A119, A128, A131, Th7; :: thesis:

end;

( k = 2 or 2 <= k - 1 ) by A92, A104, A102, NAT_1:8;
then ( k = 2 or 2 + 1 <= (k - 1) + 1 ) by XREAL_1:6;
hence ex b₁ being Element of the Lines of (G_ (k,X)) st {r,s,t} on b₁ by A123, A127; :: thesis: