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 b_{1}, b_{2}, b_{3}, b_{4}, b_{5}, b_{6}, b_{7}, b_{8}, b_{9} being Element of the Lines of (G_ (k,X)) holds

( not {o,b1,a1} on b_{1} or not {o,a2,b2} on b_{2} or not {o,a3,b3} on b_{3} or not {a3,a2,t} on b_{4} or not {a3,r,a1} on b_{5} or not {a2,s,a1} on b_{6} or not {t,b2,b3} on b_{7} or not {b1,r,b3} on b_{8} or not {b1,s,b2} on b_{9} or not b_{1},b_{2},b_{3} 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 b_{10} being Element of the Lines of (G_ (k,X)) st {r,s,t} on b_{10} )

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 b_{1} being Element of the Lines of (G_ (k,X)) st {r,s,t} on b_{1} )

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 b_{1} being Element of the Lines of (G_ (k,X)) st {r,s,t} on b_{1}

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 )

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 )

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 )

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

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 )

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

then ( k = 2 or 2 + 1 <= (k - 1) + 1 ) by XREAL_1:6;

hence ex b_{1} being Element of the Lines of (G_ (k,X)) st {r,s,t} on b_{1}
by A123, A127; :: thesis: verum

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 b

( not {o,b1,a1} on b

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 b

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 b

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

A52:
( s on A3 & s on B3 )
by A8, A11, INCSP_1:2;
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 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: verum

end;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: verum

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

then consider salpha being POINT of (G_ (k,X)) such that
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 A13, A14, A15, A16, A59, A27, A36, A48, A26, A35, INCSP_1:def 10;

hence contradiction by A12, ZFMISC_1:def 5; :: thesis: verum

end;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: verum

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

then
r \/ s = (((a3 /\ b3) \/ (a1 /\ b1)) \/ (a1 /\ b1)) \/ (a2 /\ b2)
by A62, A64, XBOOLE_1:4;
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: contradiction

( {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: verum

end;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: contradiction

( {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: verum

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

then A110:
k - 2 is Element of NAT
by A102, NAT_1:21;
assume A105:
k = 1
; :: thesis: contradiction

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: verum

end;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: verum

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

A126:
r is finite
by A115;
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 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: verum

end;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: verum

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

proof

( k = 2 or 2 <= k - 1 )
by A92, A104, A102, NAT_1:8;
A128:
( card ((r \/ s) \/ t) = k + 1 implies 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;proof

A131:
( card ((r \/ s) \/ t) = k implies ex O being LINE of (G_ (k,X)) st {r,s,t} on O )
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 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: verum

end;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: verum

proof

assume
3 <= k
; :: thesis: ex O being LINE of (G_ (k,X)) st {r,s,t} on O
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 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: verum

end;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: verum

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

then ( k = 2 or 2 + 1 <= (k - 1) + 1 ) by XREAL_1:6;

hence ex b