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:
A3: the Points of (G_ (k,X)) = { A where A is Subset of X : card A = k } by A1, A2, Def1;
A4: the Lines of (G_ (k,X)) = { L where L is Subset of X : card L = k + 1 } by A1, A2, Def1;
let A1, A2, A3, A4, A5, A6 be POINT of (G_ (k,X)); :: thesis:
let L1, L2, L3, L4 be LINE of (G_ (k,X)); :: thesis:
assume that
A5: A1 on L1 and
A6: A2 on L1 and
A7: A3 on L2 and
A8: A4 on L2 and
A9: A5 on L1 and
A10: A5 on L2 and
A11: A1 on L3 and
A12: A3 on L3 and
A13: A2 on L4 and
A14: A4 on L4 and
A15: not A5 on L3 and
A16: not A5 on L4 and
A17: L1 <> L2 and
A18: L3 <> L4 ; :: thesis:
A19: ( A1 c= L1 & A2 c= L1 ) by A1, A2, A5, A6, Th10;
A20: ( A3 c= L2 & A4 c= L2 ) by A1, A2, A7, A8, Th10;
A21: ( A5 c= L1 & A5 c= L2 ) by A1, A2, A9, A10, Th10;
A5 in the Points of (G_ (k,X)) ;
then A22: ex B5 being Subset of X st
( B5 = A5 & card B5 = k ) by A3;
A2 in the Points of (G_ (k,X)) ;
then A23: ex B2 being Subset of X st
( B2 = A2 & card B2 = k ) by A3;
then A24: A2 is finite ;
reconsider k1 = k - 1 as Element of NAT by A1, NAT_1:20;
L3 in the Lines of (G_ (k,X)) ;
then A25: ex K3 being Subset of X st
( K3 = L3 & card K3 = k + 1 ) by A4;
then A26: L3 is finite ;
L4 in the Lines of (G_ (k,X)) ;
then ex K4 being Subset of X st
( K4 = L4 & card K4 = k + 1 ) by A4;
then card (L3 /\ L4) in Segm (k + 1) by A25, A18, Th1;
then card (L3 /\ L4) in succ (Segm k) by NAT_1:38;
then A27: card (L3 /\ L4) c= k by ORDINAL1:22;
A1 in the Points of (G_ (k,X)) ;
then A28: ex B1 being Subset of X st
( B1 = A1 & card B1 = k ) by A3;
then A29: A1 is finite ;
G_ (k,X) is Vebleian by A1, A2, Th11;
then consider A6 being POINT of (G_ (k,X)) such that
A30: A6 on L3 and
A31: A6 on L4 by A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17;
A6 in the Points of (G_ (k,X)) ;
then A32: ex a6 being Subset of X st
( a6 = A6 & card a6 = k ) by A3;
then A33: A6 is finite ;
A34: ( A6 c= L3 & A6 c= L4 ) by A1, A2, A30, A31, Th10;
then A6 c= L3 /\ L4 by XBOOLE_1:19;
then k c= card (L3 /\ L4) by A32, CARD_1:11;
then card (L3 /\ L4) = k by A27, XBOOLE_0:def 10;
then A35: L3 /\ L4 = A6 by A32, A34, A26, CARD_2:102, XBOOLE_1:19;
L2 in the Lines of (G_ (k,X)) ;
then A36: ex K2 being Subset of X st
( K2 = L2 & card K2 = k + 1 ) by A4;
then A37: L2 is finite ;
A4 in the Points of (G_ (k,X)) ;
then A38: ex B4 being Subset of X st
( B4 = A4 & card B4 = k ) by A3;
then A39: A4 is finite ;
L1 in the Lines of (G_ (k,X)) ;
then A40: ex K1 being Subset of X st
( K1 = L1 & card K1 = k + 1 ) by A4;
then A41: L1 is finite ;
A3 in the Points of (G_ (k,X)) ;
then A42: ex B3 being Subset of X st
( B3 = A3 & card B3 = k ) by A3;
then A43: A3 is finite ;
A44: ( A3 c= L3 & A4 c= L4 ) by A1, A2, A12, A14, Th10;
then A45: A3 /\ A4 c= A6 by A35, XBOOLE_1:27;
A46: ( A1 c= L3 & A2 c= L4 ) by A1, A2, A11, A13, Th10;
then A47: A1 /\ A2 c= A6 by A35, XBOOLE_1:27;
then A48: (A1 /\ A2) \/ (A3 /\ A4) c= A6 by A45, XBOOLE_1:8;
A49: ( not A6 on L1 implies A6 = (A1 /\ A2) \/ (A3 /\ A4) )

proof

assume A50: not A6 on L1 ; :: thesis:
A51: ( not A6 on L2 implies A6 = (A1 /\ A2) \/ (A3 /\ A4) )

proof

A52: A1 \/ A2 c= L1 by A19, XBOOLE_1:8;
then A53: card (A1 \/ A2) c= k + 1 by A40, CARD_1:11;
A54: A3 \/ A4 c= L2 by A20, XBOOLE_1:8;
then A55: card (A3 \/ A4) c= k + 1 by A36, CARD_1:11;
A56: card A3 = (k - 1) + 1 by A42;
card ((A1 /\ A2) \/ (A3 /\ A4)) c= k by A32, A48, CARD_1:11;
then card ((A1 /\ A2) \/ (A3 /\ A4)) in succ k by ORDINAL1:22;
then ( card ((A1 /\ A2) \/ (A3 /\ A4)) in Segm (k1 + 1) or card ((A1 /\ A2) \/ (A3 /\ A4)) = k ) by ORDINAL1:8;
then ( card ((A1 /\ A2) \/ (A3 /\ A4)) in succ (Segm k1) or card ((A1 /\ A2) \/ (A3 /\ A4)) = k ) by NAT_1:38;
then A57: ( card ((A1 /\ A2) \/ (A3 /\ A4)) c= Segm k1 or card ((A1 /\ A2) \/ (A3 /\ A4)) = k ) by ORDINAL1:22;
A58: card A1 = (k - 1) + 1 by A28;
assume A59: not A6 on L2 ; :: thesis:
A60: ( A1 <> A2 & A3 <> A4 )

proof

assume ( A1 = A2 or A3 = A4 ) ; :: thesis:
then ( ( {A1,A6} on L3 & {A1,A6} on L4 ) or ( {A3,A6} on L3 & {A3,A6} on L4 ) ) by A11, A12, A13, A14, A30, A31, INCSP_1:1;
hence contradiction by A5, A7, A18, A50, A59, INCSP_1:def 10; :: thesis:

end;

then k + 1 c= card (A1 \/ A2) by A28, A23, Th1;
then card (A1 \/ A2) = k1 + (2 * 1) by A53, XBOOLE_0:def 10;
then A61: card (A1 /\ A2) = k1 by A23, A58, Th2;
k + 1 c= card (A3 \/ A4) by A42, A38, A60, Th1;
then card (A3 \/ A4) = k1 + (2 * 1) by A55, XBOOLE_0:def 10;
then A62: card (A3 /\ A4) = k1 by A38, A56, Th2;
A63: not card ((A1 /\ A2) \/ (A3 /\ A4)) = k - 1

proof

A64: A5 c= L1 /\ L2 by A21, XBOOLE_1:19;
A65: (A1 /\ A2) /\ (A3 /\ A4) c= A1 /\ A2 by XBOOLE_1:17;
A66: ((A1 /\ A2) /\ A3) /\ A4 = (A1 /\ A2) /\ (A3 /\ A4) by XBOOLE_1:16;
A67: A1 /\ A2 c= A1 by XBOOLE_1:17;
then A68: A1 = (((A1 /\ A2) /\ A3) /\ A4) \/ (A1 \ (((A1 /\ A2) /\ A3) /\ A4)) by A65, A66, XBOOLE_1:1, XBOOLE_1:45;
assume A69: card ((A1 /\ A2) \/ (A3 /\ A4)) = k - 1 ; :: thesis:
then card ((A1 /\ A2) \/ (A3 /\ A4)) = k1 + (2 * 0) ;
then A70: card ((A1 /\ A2) /\ (A3 /\ A4)) = k1 by A61, A62, Th2;
then A71: (A1 /\ A2) /\ (A3 /\ A4) = (A1 /\ A2) \/ (A3 /\ A4) by A29, A43, A69, CARD_2:102, XBOOLE_1:29;
then card (A1 \ (((A1 /\ A2) /\ A3) /\ A4)) = k - (k - 1) by A28, A29, A69, A67, A65, A66, CARD_2:44, XBOOLE_1:1;
then consider x1 being object such that
A72: A1 \ (((A1 /\ A2) /\ A3) /\ A4) = {x1} by CARD_2:42;
A73: A1 /\ A2 c= A2 by XBOOLE_1:17;
then A74: A2 = (((A1 /\ A2) /\ A3) /\ A4) \/ (A2 \ (((A1 /\ A2) /\ A3) /\ A4)) by A65, A66, XBOOLE_1:1, XBOOLE_1:45;
card (A2 \ (((A1 /\ A2) /\ A3) /\ A4)) = k - (k - 1) by A23, A24, A69, A73, A65, A71, A66, CARD_2:44, XBOOLE_1:1;
then consider x2 being object such that
A75: A2 \ (((A1 /\ A2) /\ A3) /\ A4) = {x2} by CARD_2:42;
x1 in {x1} by TARSKI:def 1;
then A76: not x1 in ((A1 /\ A2) /\ A3) /\ A4 by A72, XBOOLE_0:def 5;
A77: (A1 /\ A2) /\ (A3 /\ A4) c= A3 /\ A4 by XBOOLE_1:17;
A78: A3 /\ A4 c= A4 by XBOOLE_1:17;
then A79: A4 = (((A1 /\ A2) /\ A3) /\ A4) \/ (A4 \ (((A1 /\ A2) /\ A3) /\ A4)) by A77, A66, XBOOLE_1:1, XBOOLE_1:45;
card (A4 \ (((A1 /\ A2) /\ A3) /\ A4)) = k - (k - 1) by A38, A39, A69, A78, A77, A71, A66, CARD_2:44, XBOOLE_1:1;
then consider x4 being object such that
A80: A4 \ (((A1 /\ A2) /\ A3) /\ A4) = {x4} by CARD_2:42;
A81: A3 /\ A4 c= A3 by XBOOLE_1:17;
then A82: A3 = (((A1 /\ A2) /\ A3) /\ A4) \/ (A3 \ (((A1 /\ A2) /\ A3) /\ A4)) by A77, A66, XBOOLE_1:1, XBOOLE_1:45;
card (A3 \ (((A1 /\ A2) /\ A3) /\ A4)) = k - (k - 1) by A42, A43, A69, A81, A77, A71, A66, CARD_2:44, XBOOLE_1:1;
then consider x3 being object such that
A83: A3 \ (((A1 /\ A2) /\ A3) /\ A4) = {x3} by CARD_2:42;
( k + 1 c= card (A3 \/ A4) & card (A3 \/ A4) c= k + 1 ) by A42, A38, A36, A60, A54, Th1, CARD_1:11;
then card (A3 \/ A4) = k + 1 by XBOOLE_0:def 10;
then A3 \/ A4 = L2 by A36, A20, A37, CARD_2:102, XBOOLE_1:8;
then A84: L2 = (((A1 /\ A2) /\ A3) /\ A4) \/ ({x3} \/ {x4}) by A83, A80, A82, A79, XBOOLE_1:5;
then A85: L2 = (((A1 /\ A2) /\ A3) /\ A4) \/ {x3,x4} by ENUMSET1:1;
A86: ( x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 )

proof

assume ( x1 = x3 or x1 = x4 or x2 = x3 or x2 = x4 ) ; :: thesis:
then ( ( {A1,A5} on L1 & {A1,A5} on L2 ) or ( {A1,A5} on L1 & {A1,A5} on L2 ) or ( {A2,A5} on L1 & {A2,A5} on L2 ) or ( {A2,A5} on L1 & {A2,A5} on L2 ) ) by A5, A6, A7, A8, A9, A10, A72, A75, A83, A80, A68, A74, A82, A79, INCSP_1:1;
hence contradiction by A11, A13, A15, A16, A17, INCSP_1:def 10; :: thesis:

end;

x2 in {x2} by TARSKI:def 1;
then A87: not x2 in ((A1 /\ A2) /\ A3) /\ A4 by A75, XBOOLE_0:def 5;
( k + 1 c= card (A1 \/ A2) & card (A1 \/ A2) c= k + 1 ) by A28, A23, A40, A60, A52, Th1, CARD_1:11;
then card (A1 \/ A2) = k + 1 by XBOOLE_0:def 10;
then A1 \/ A2 = L1 by A40, A19, A41, CARD_2:102, XBOOLE_1:8;
then A88: L1 = (((A1 /\ A2) /\ A3) /\ A4) \/ ({x1} \/ {x2}) by A72, A75, A68, A74, XBOOLE_1:5;
then A89: L1 = (((A1 /\ A2) /\ A3) /\ A4) \/ {x1,x2} by ENUMSET1:1;
A90: L1 /\ L2 c= ((A1 /\ A2) /\ A3) /\ A4

proof

assume not L1 /\ L2 c= ((A1 /\ A2) /\ A3) /\ A4 ; :: thesis:
then consider x being object such that
A91: x in L1 /\ L2 and
A92: not x in ((A1 /\ A2) /\ A3) /\ A4 ;
x in L1 by A91, XBOOLE_0:def 4;
then A93: x in {x1,x2} by A89, A92, XBOOLE_0:def 3;
x in L2 by A91, XBOOLE_0:def 4;
then ( x1 in L2 or x2 in L2 ) by A93, TARSKI:def 2;
then ( x1 in {x3,x4} or x2 in {x3,x4} ) by A85, A76, A87, XBOOLE_0:def 3;
hence contradiction by A86, TARSKI:def 2; :: thesis:

end;

A94: ((A1 /\ A2) /\ A3) /\ A4 c= L2 by A84, XBOOLE_1:10;
((A1 /\ A2) /\ A3) /\ A4 c= L1 by A88, XBOOLE_1:10;
then ((A1 /\ A2) /\ A3) /\ A4 c= L1 /\ L2 by A94, XBOOLE_1:19;
then L1 /\ L2 = ((A1 /\ A2) /\ A3) /\ A4 by A90, XBOOLE_0:def 10;
then card (Segm k) c= card (Segm k1) by A22, A70, A66, A64, CARD_1:11;
then A95: k <= k1 by NAT_1:40;
k1 <= k1 + 1 by NAT_1:11;
then k = k - 1 by A95, XXREAL_0:1;
hence contradiction ; :: thesis:

end;

k - 1 c= card ((A1 /\ A2) \/ (A3 /\ A4)) by A61, CARD_1:11, XBOOLE_1:7;
then card ((A1 /\ A2) \/ (A3 /\ A4)) = k by A57, A63, XBOOLE_0:def 10;
hence A6 = (A1 /\ A2) \/ (A3 /\ A4) by A32, A33, A47, A45, CARD_2:102, XBOOLE_1:8; :: thesis:

end;

( A6 on L2 implies A6 = (A1 /\ A2) \/ (A3 /\ A4) )

proof

assume A96: A6 on L2 ; :: thesis:
A97: A4 = A6

proof

assume A98: A4 <> A6 ; :: thesis:
( {A4,A6} on L2 & {A4,A6} on L4 ) by A8, A14, A31, A96, INCSP_1:1;
hence contradiction by A10, A16, A98, INCSP_1:def 10; :: thesis:

end;

A3 = A6

proof

assume A99: A3 <> A6 ; :: thesis:
( {A3,A6} on L2 & {A3,A6} on L3 ) by A7, A12, A30, A96, INCSP_1:1;
hence contradiction by A10, A15, A99, INCSP_1:def 10; :: thesis:

end;

hence A6 = (A1 /\ A2) \/ (A3 /\ A4) by A46, A35, A97, XBOOLE_1:12, XBOOLE_1:27; :: thesis:

end;

hence A6 = (A1 /\ A2) \/ (A3 /\ A4) by A51; :: thesis:

end;

( A6 on L1 implies A6 = (A1 /\ A2) \/ (A3 /\ A4) )

proof

assume A100: A6 on L1 ; :: thesis:
A101: A1 = A6

proof

assume A102: A1 <> A6 ; :: thesis:
( {A1,A6} on L1 & {A1,A6} on L3 ) by A5, A11, A30, A100, INCSP_1:1;
hence contradiction by A9, A15, A102, INCSP_1:def 10; :: thesis:

end;

A2 = A6

proof

assume A103: A2 <> A6 ; :: thesis:
( {A2,A6} on L1 & {A2,A6} on L4 ) by A6, A13, A31, A100, INCSP_1:1;
hence contradiction by A9, A16, A103, INCSP_1:def 10; :: thesis:

end;

hence A6 = (A1 /\ A2) \/ (A3 /\ A4) by A44, A35, A101, XBOOLE_1:12, XBOOLE_1:27; :: thesis:

end;

hence ex A6 being POINT of (G_ (k,X)) st
( A6 on L3 & A6 on L4 & A6 = (A1 /\ A2) \/ (A3 /\ A4) ) by A30, A31, A49; :: thesis: