let k be Element of NAT ; :: thesis:
let X be non empty set ; :: thesis:
assume A1: ( 0 < k & k + 1 c= card X ) ; :: thesis:
then A2: k - 1 is Element of NAT by NAT_1:20;
let o, b1, a1, b2, a2, b3, a3, r, s, t be POINT of (G_ k,X); :: according to INCPROJ:def 19 :: thesis:
let C1, C2, C3, A1, A2, A3, B1, B2, B3 be LINE of (G_ k,X); :: thesis:
A3: the Points of (G_ k,X) = { A where A is Subset of X : card A = k } by A1, Def1;
A4: the Lines of (G_ k,X) = { L where L is Subset of X : card L = k + 1 } by A1, Def1;
o in the Points of (G_ k,X) ;
then consider o1 being Subset of X such that
A5: ( o1 = o & card o1 = k ) by A3;
a1 in the Points of (G_ k,X) ;
then consider a11 being Subset of X such that
A6: ( a11 = a1 & card a11 = k ) by A3;
a2 in the Points of (G_ k,X) ;
then consider a12 being Subset of X such that
A7: ( a12 = a2 & card a12 = k ) by A3;
a3 in the Points of (G_ k,X) ;
then consider a13 being Subset of X such that
A8: ( a13 = a3 & card a13 = k ) by A3;
b1 in the Points of (G_ k,X) ;
then consider b11 being Subset of X such that
A9: ( b11 = b1 & card b11 = k ) by A3;
b2 in the Points of (G_ k,X) ;
then consider b12 being Subset of X such that
A10: ( b12 = b2 & card b12 = k ) by A3;
b3 in the Points of (G_ k,X) ;
then consider b13 being Subset of X such that
A11: ( b13 = b3 & card b13 = k ) by A3;
C1 in the Lines of (G_ k,X) ;
then consider C11 being Subset of X such that
A12: ( C11 = C1 & card C11 = k + 1 ) by A4;
C2 in the Lines of (G_ k,X) ;
then consider C12 being Subset of X such that
A13: ( C12 = C2 & card C12 = k + 1 ) by A4;
C3 in the Lines of (G_ k,X) ;
then consider C13 being Subset of X such that
A14: ( C13 = C3 & card C13 = k + 1 ) by A4;
assume A15: ( {o,b1,a1} on C1 & {o,a2,b2} on C2 & {o,a3,b3} on C3 & {a3,a2,t} on A1 & {a3,r,a1} on A2 & {a2,s,a1} on A3 & {t,b2,b3} on B1 & {b1,r,b3} on B2 & {b1,s,b2} on B3 & C1,C2,C3 are_mutually_different & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a1 <> b1 & a2 <> b2 & a3 <> b3 ) ; :: thesis:
then A16: ( o on C1 & b1 on C1 & a1 on C1 & o on C2 & a2 on C2 & b2 on C2 & o on C3 & a3 on C3 & b3 on C3 & a3 on A1 & a2 on A1 & t on A1 & a3 on A2 & r on A2 & a1 on A2 & a2 on A3 & s on A3 & a1 on A3 & t on B1 & b2 on B1 & b3 on B1 & b1 on B2 & r on B2 & b3 on B2 & b1 on B3 & s on B3 & b2 on B3 ) by INCSP_1:12;
then A17: ( {o,a1} on C1 & {o,a2} on C2 & {o,a3} on C3 & {a2,a3} on A1 & {a1,a3} on A2 & {a1,a2} on A3 & {a1,b1} on C1 & {a2,b2} on C2 & {a3,b3} on C3 & {o,b1} on C1 & {o,b2} on C2 & {o,b3} on C3 & {b2,b3} on B1 & {b1,b3} on B2 & {b1,b2} on B3 ) by INCSP_1:11;
A18: ( C1 <> C2 & C2 <> C3 & C1 <> C3 ) by A15, ZFMISC_1:def 5;
A19: ( o c= C1 & b1 c= C1 & a1 c= C1 & o c= C2 & a2 c= C2 & b2 c= C2 & o c= C3 & a3 c= C3 & b3 c= C3 & a3 c= A1 & a2 c= A1 & t c= A1 & a3 c= A2 & r c= A2 & a1 c= A2 & a2 c= A3 & s c= A3 & a1 c= A3 & t c= B1 & b2 c= B1 & b3 c= B1 & b1 c= B2 & r c= B2 & b3 c= B2 & b1 c= B3 & s c= B3 & b2 c= B3 ) by A1, A16, Th10;
( 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 A16, INCSP_1:11;
then ( b3 on C1 or b1 on C2 or b2 on C3 ) by A15, A16, A17, INCSP_1:def 10;
then ( {o,b3} on C1 or {o,b1} on C2 or {o,b2} on C3 ) by A16, INCSP_1:11;
hence contradiction by A15, A17, A18, INCSP_1:def 10; :: thesis:

end;

then A20: ( not a1 c= B2 & not a2 c= B3 & not a3 c= B1 ) by A1, Th10;
then consider z1 being set such that
A21: ( z1 in a1 & not z1 in B2 ) by TARSKI:def 3;
consider z2 being set such that
A22: ( z2 in a2 & not z2 in B3 ) by A20, TARSKI:def 3;
consider z3 being set such that
A23: ( z3 in a3 & not z3 in B1 ) by A20, TARSKI:def 3;
A24: ( A1 <> B1 & A2 <> B2 & A3 <> B3 ) by A19, A21, A22, A23;
A25: ( 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 A16, INCSP_1:11;
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 A15, A17, INCSP_1:def 10;
hence contradiction by A15, ZFMISC_1:def 5; :: thesis:

end;

then consider salpha being POINT of (G_ k,X) such that
A26: ( salpha on A3 & salpha on B3 & salpha = (a1 /\ b1) \/ (a2 /\ b2) ) by A1, A16, A18, A24, Th12;
consider ralpha being POINT of (G_ k,X) such that
A27: ( ralpha on B2 & ralpha on A2 & ralpha = (a1 /\ b1) \/ (a3 /\ b3) ) by A1, A16, A18, A24, A25, Th12;
consider talpha being POINT of (G_ k,X) such that
A28: ( talpha on A1 & talpha on B1 & talpha = (a2 /\ b2) \/ (a3 /\ b3) ) by A1, A16, A18, A24, A25, Th12;
A29: ( r = ralpha & s = salpha & t = talpha )

proof

assume A30: ( r <> ralpha or s <> salpha or t <> talpha ) ; :: thesis:
( {r,ralpha} on A2 & {r,ralpha} on B2 & {s,salpha} on A3 & {s,salpha} on B3 & {t,talpha} on A1 & {t,talpha} on B1 ) by A16, A26, A27, A28, INCSP_1:11;
hence contradiction by A24, A30, INCSP_1:def 10; :: thesis:

end;

r in the Points of (G_ k,X) ;
then consider r1 being Subset of X such that
A31: ( r1 = r & card r1 = k ) by A3;
s in the Points of (G_ k,X) ;
then consider s1 being Subset of X such that
A32: ( s1 = s & card s1 = k ) by A3;
t in the Points of (G_ k,X) ;
then consider t1 being Subset of X such that
A33: ( t1 = t & card t1 = k ) by A3;
( a1 \/ b1 c= C1 & a2 \/ b2 c= C2 & a3 \/ b3 c= C3 ) by A19, XBOOLE_1:8;
then ( k + 1 c= card (a1 \/ b1) & card (a1 \/ b1) c= k + 1 & k + 1 c= card (a2 \/ b2) & card (a2 \/ b2) c= k + 1 & k + 1 c= card (a3 \/ b3) & card (a3 \/ b3) c= k + 1 ) by A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, Th1, CARD_1:27;
then A34: ( card (a1 \/ b1) = (k - 1) + (2 * 1) & card (a2 \/ b2) = (k - 1) + (2 * 1) & card (a3 \/ b3) = (k - 1) + (2 * 1) & card a1 = (k - 1) + 1 & card a2 = (k - 1) + 1 & card a3 = (k - 1) + 1 & card b1 = (k - 1) + 1 & card b2 = (k - 1) + 1 & card b3 = (k - 1) + 1 ) by A6, A7, A8, A9, A10, A11, XBOOLE_0:def 10;
then A35: ( card (a1 /\ b1) = k - 1 & card (a2 /\ b2) = k - 1 & card (a3 /\ b3) = k - 1 ) by A2, Th2;
r \/ s = (((a3 /\ b3) \/ (a1 /\ b1)) \/ (a1 /\ b1)) \/ (a2 /\ b2) by A26, A27, A29, XBOOLE_1:4;
then r \/ s = ((a3 /\ b3) \/ ((a1 /\ b1) \/ (a1 /\ b1))) \/ (a2 /\ b2) by XBOOLE_1:4;
then ( r \/ s = ((a1 /\ b1) \/ (a3 /\ b3)) \/ (a2 /\ b2) & (a3 /\ b3) \/ (a2 /\ b2) c= (a1 /\ b1) \/ ((a3 /\ b3) \/ (a2 /\ b2)) & ((a1 /\ b1) \/ (a3 /\ b3)) \/ (a2 /\ b2) = (a1 /\ b1) \/ ((a3 /\ b3) \/ (a2 /\ b2)) ) by XBOOLE_1:4, XBOOLE_1:7;
then A36: (r \/ s) \/ t = ((a1 /\ b1) \/ (a3 /\ b3)) \/ (a2 /\ b2) by A28, A29, XBOOLE_1:12;
A37: not k = 1

proof

assume A38: k = 1 ; :: thesis:
then consider z1 being set such that
A39: o = {z1} by A5, CARD_2:60;
consider z2 being set such that
A40: a1 = {z2} by A6, A38, CARD_2:60;
consider z3 being set such that
A41: b1 = {z3} by A9, A38, CARD_2:60;
A42: card {z1,z2,z3} = 3 by A15, A39, A40, A41, CARD_2:77;
o \/ a1 c= C1 by A19, XBOOLE_1:8;
then (o \/ a1) \/ b1 c= C1 by A19, XBOOLE_1:8;
then {z1,z2} \/ b1 c= C1 by A39, A40, ENUMSET1:41;
then {z1,z2,z3} c= C1 by A41, ENUMSET1:43;
then ( 3 c= card C1 & card C1 = 2 ) by A12, A38, A42, CARD_1:27;
hence contradiction by NAT_1:40; :: thesis:

end;

0 + 1 < k + 1 by A1, XREAL_1:10;
then 1 <= (k - 1) + 1 by NAT_1:13;
then ( 1 <= k - 1 or k = 1 ) by A2, NAT_1:8;
then A43: ( 1 + 1 <= (k - 1) + 1 or k = 1 ) by XREAL_1:8;
then ( k = 2 or 2 <= k - 1 ) by A2, A37, NAT_1:8;
then A44: ( k = 2 or 2 + 1 <= (k - 1) + 1 ) by XREAL_1:8;
A45: k - 2 is Element of NAT by A37, A43, NAT_1:21;
( card ((a1 /\ b1) \/ (a3 /\ b3)) = (k - 2) + (2 * 1) & card (a1 /\ b1) = (k - 2) + 1 & card ((a1 /\ b1) \/ (a2 /\ b2)) = (k - 2) + (2 * 1) & card (a2 /\ b2) = (k - 2) + 1 & card ((a2 /\ b2) \/ (a3 /\ b3)) = (k - 2) + (2 * 1) & card (a3 /\ b3) = (k - 2) + 1 ) by A2, A26, A27, A28, A29, A31, A32, A33, A34, Th2;
then A46: ( card ((a1 /\ b1) /\ (a3 /\ b3)) = k - 2 & card ((a2 /\ b2) /\ (a3 /\ b3)) = k - 2 & card ((a1 /\ b1) /\ (a2 /\ b2)) = k - 2 ) by A45, Th2;
( r \/ s c= X & k = card k ) by A31, A32, XBOOLE_1:8;
then A47: ( (r \/ s) \/ t c= X & r is finite & s is finite & t is finite ) by A31, A32, A33, XBOOLE_1:8;
( r c= r \/ (s \/ t) & s c= s \/ (r \/ t) & t c= t \/ (r \/ s) & r \/ (s \/ t) is finite ) by A47, XBOOLE_1:7;
then A48: ( r c= (r \/ s) \/ t & s c= (r \/ s) \/ t & t c= (r \/ s) \/ t & (r \/ s) \/ t is finite ) by XBOOLE_1:4;
A49: ( 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 A35, A36, A46, Th7;
then (r \/ s) \/ t in the Lines of (G_ k,X) by A4, A47;
then consider O being LINE of (G_ k,X) such that
A50: O = (r \/ s) \/ t ;
( r on O & s on O & t on O ) by A1, A48, A50, Th10;
then {r,s,t} on O by INCSP_1:12;
hence ex O being LINE of (G_ k,X) st {r,s,t} on O ; :: thesis:

end;

( 3 <= k implies ex O being LINE of (G_ k,X) st {r,s,t} on O )

proof

assume A51: 3 <= k ; :: thesis:
A52: ( 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 A4, A47;
then consider O being LINE of (G_ k,X) such that
A53: O = (r \/ s) \/ t ;
( r on O & s on O & t on O ) by A1, A48, A53, Th10;
then {r,s,t} on O by INCSP_1:12;
hence ex O being LINE of (G_ k,X) st {r,s,t} on O ; :: thesis:

end;

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

proof

assume card ((r \/ s) \/ t) = k ; :: thesis:
then ( r = (r \/ s) \/ t & s = (r \/ s) \/ t & t = (r \/ s) \/ t ) by A31, A32, A33, A48, CARD_FIN:1;
then {r,s,t} on A1 by A16, INCSP_1:12;
hence ex O being LINE of (G_ k,X) st {r,s,t} on O ; :: thesis:

end;

hence ex O being LINE of (G_ k,X) st {r,s,t} on O by A35, A36, A43, A46, A51, A52, Th7; :: thesis:

end;

hence ex b₁ being Element of the Lines of (G_ k,X) st {r,s,t} on b₁ by A44, A49; :: thesis: