let k be Element of NAT ; :: thesis: for X being non empty set st 0 < k & k + 1 c= card X holds
G_ (k,X) is Desarguesian

let X be non empty set ; :: thesis: ( 0 < k & k + 1 c= card X implies G_ (k,X) is Desarguesian )
assume that
A1: 0 < k and
A2: k + 1 c= card X ; :: thesis: G_ (k,X) is Desarguesian
let o, b1, a1, b2, a2, b3, a3, r, s, t be POINT of (G_ (k,X)); :: according to INCPROJ:def 13 :: thesis: for b1, b2, b3, b4, b5, b6, b7, b8, b9 being Element of the Lines of (G_ (k,X)) holds
( not {o,b1,a1} on b1 or not {o,a2,b2} on b2 or not {o,a3,b3} on b3 or not {a3,a2,t} on b4 or not {a3,r,a1} on b5 or not {a2,s,a1} on b6 or not {t,b2,b3} on b7 or not {b1,r,b3} on b8 or not {b1,s,b2} on b9 or not b1,b2,b3 are_mutually_distinct or o = a1 or o = a2 or o = a3 or o = b1 or o = b2 or o = b3 or a1 = b1 or a2 = b2 or a3 = b3 or ex b10 being Element of the Lines of (G_ (k,X)) st {r,s,t} on b10 )

let C1, C2, C3, A1, A2, A3, B1, B2, B3 be LINE of (G_ (k,X)); :: thesis: ( not {o,b1,a1} on C1 or not {o,a2,b2} on C2 or not {o,a3,b3} on C3 or not {a3,a2,t} on A1 or not {a3,r,a1} on A2 or not {a2,s,a1} on A3 or not {t,b2,b3} on B1 or not {b1,r,b3} on B2 or not {b1,s,b2} on B3 or not C1,C2,C3 are_mutually_distinct or o = a1 or o = a2 or o = a3 or o = b1 or o = b2 or o = b3 or a1 = b1 or a2 = b2 or a3 = b3 or ex b1 being Element of the Lines of (G_ (k,X)) st {r,s,t} on b1 )
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: ex b1 being Element of the Lines of (G_ (k,X)) st {r,s,t} on b1
A20: o on C1 by ;
A21: b2 on C2 by ;
then A22: b2 c= C2 by A1, A2, Th10;
A23: a2 on C2 by ;
then A24: {a2,b2} on C2 by ;
A25: o on C2 by ;
then A26: {o,b2} on C2 by ;
A27: {o,a2} on C2 by ;
A28: ( a3 on A1 & a2 on A1 ) by ;
A29: b3 on B2 by ;
A30: b3 on C3 by ;
then A31: b3 c= C3 by A1, A2, Th10;
A32: a3 on C3 by ;
then A33: {a3,b3} on C3 by ;
A34: o on C3 by ;
then A35: {o,b3} on C3 by ;
A36: {o,a3} on C3 by ;
A37: ( a3 on A2 & a1 on A2 ) by ;
A38: b1 on B3 by ;
A39: C1 <> C3 by ;
A40: b1 on B2 by ;
A41: C2 <> C3 by ;
A42: b3 on B1 by ;
A43: C1 <> C2 by ;
A44: b2 on B1 by ;
A45: a1 on C1 by ;
then A46: a1 c= C1 by A1, A2, Th10;
A47: b1 on C1 by ;
then A48: {o,b1} on C1 by ;
A49: b2 on B3 by ;
A50: {a1,b1} on C1 by ;
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: contradiction
then ( {a1,b1} on B2 or {a2,b2} on B3 or {a3,b3} on B1 ) by ;
then ( b3 on C1 or b1 on C2 or b2 on C3 ) by ;
then ( {o,b3} on C1 or {o,b1} on C2 or {o,b2} on C3 ) by ;
hence contradiction by A15, A16, A48, A26, A35, A43, A41, A39, INCSP_1:def 10; :: thesis: verum
end;
A52: ( s on A3 & s on B3 ) by ;
A53: t on B1 by ;
A54: ( r on A2 & r on B2 ) by ;
A55: t on A1 by ;
A56: a1 on A3 by ;
A57: a2 on A3 by ;
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 ;
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: contradiction
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 ;
hence contradiction by A12, ZFMISC_1:def 5; :: thesis: verum
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 ;
A69: ( r = ralpha & s = salpha & t = talpha )
proof
A70: ( {s,salpha} on A3 & {s,salpha} on B3 ) by ;
A71: ( {r,ralpha} on A2 & {r,ralpha} on B2 ) by ;
assume A72: ( r <> ralpha or s <> salpha or t <> talpha ) ; :: thesis: contradiction
( {t,talpha} on A1 & {t,talpha} on B1 ) by ;
hence contradiction by A57, A51, A68, A72, A71, A70, INCSP_1:def 10; :: thesis: verum
end;
then r \/ s = (((a3 /\ b3) \/ (a1 /\ b1)) \/ (a1 /\ b1)) \/ (a2 /\ b2) by ;
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 ;
a2 c= C2 by A1, A2, A23, Th10;
then A74: a2 \/ b2 c= C2 by ;
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 ;
then A78: card (a1 \/ b1) c= k + 1 by ;
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 ;
then A91: card (a1 \/ b1) = (k - 1) + (2 * 1) by ;
A92: k - 1 is Element of NAT by ;
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 ;
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 ;
then A95: card (a2 \/ b2) = (k - 1) + (2 * 1) by ;
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 ;
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 ;
then 1 <= (k - 1) + 1 by NAT_1:13;
then ( 1 <= k - 1 or k = 1 ) by ;
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: contradiction
then consider z1 being object such that
A106: o = {z1} by ;
consider z3 being object such that
A107: b1 = {z3} by ;
consider z2 being object such that
A108: a1 = {z2} by ;
o \/ a1 c= C1 by ;
then (o \/ a1) \/ b1 c= C1 by ;
then {z1,z2} \/ b1 c= C1 by ;
then A109: {z1,z2,z3} c= C1 by ;
card {z1,z2,z3} = 3 by ;
then Segm 3 c= Segm (card C1) by ;
hence contradiction by A76, A105, NAT_1:39; :: thesis: verum
end;
then A110: k - 2 is Element of NAT by ;
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 ;
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 ;
then A113: card (a3 \/ b3) = (k - 1) + (2 * 1) by ;
then A114: card (a3 /\ b3) = k - 1 by ;
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 ;
then A116: (r \/ s) \/ t c= X by ;
A117: card (a3 /\ b3) = (k - 2) + 1 by ;
A118: card (a1 /\ b1) = (k - 2) + 1 by A92, A81, A91, A98, Th2;
card ((a1 /\ b1) \/ (a2 /\ b2)) = (k - 2) + (2 * 1) by ;
then A119: card ((a1 /\ b1) /\ (a2 /\ b2)) = k - 2 by ;
card ((a2 /\ b2) \/ (a3 /\ b3)) = (k - 2) + (2 * 1) by ;
then A120: card ((a2 /\ b2) /\ (a3 /\ b3)) = k - 2 by ;
card ((a1 /\ b1) \/ (a3 /\ b3)) = (k - 2) + (2 * 1) by ;
then A121: card ((a1 /\ b1) /\ (a3 /\ b3)) = k - 2 by ;
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: ex O being LINE of (G_ (k,X)) st {r,s,t} on O
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 ;
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 ;
hence ex O being LINE of (G_ (k,X)) st {r,s,t} on O ; :: thesis: verum
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: ex O being LINE of (G_ (k,X)) st {r,s,t} on O
then (r \/ s) \/ t in the Lines of (G_ (k,X)) by ;
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 ;
hence ex O being LINE of (G_ (k,X)) st {r,s,t} on O ; :: thesis: verum
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: ex O being LINE of (G_ (k,X)) st {r,s,t} on O
then A133: t = (r \/ s) \/ t by ;
( r = (r \/ s) \/ t & s = (r \/ s) \/ t ) by ;
then {r,s,t} on A1 by ;
hence ex O being LINE of (G_ (k,X)) st {r,s,t} on O ; :: thesis: verum
end;
assume 3 <= k ; :: thesis: ex O being LINE of (G_ (k,X)) st {r,s,t} on O
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: verum
end;
( k = 2 or 2 <= k - 1 ) by ;
then ( k = 2 or 2 + 1 <= (k - 1) + 1 ) by XREAL_1:6;
hence ex b1 being Element of the Lines of (G_ (k,X)) st {r,s,t} on b1 by ; :: thesis: verum