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

proof

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

proof

A53: A1 \/ A2 c= L1 by A19, XBOOLE_1:8;
then A54: card (A1 \/ A2) c= k + 1 by A41, CARD_1:11;
A55: A3 \/ A4 c= L2 by A20, XBOOLE_1:8;
then A56: card (A3 \/ A4) c= k + 1 by A37, CARD_1:11;
A57: card A3 = (k - 1) + 1 by A43;
card ((A1 /\ A2) \/ (A3 /\ A4)) c= k by A33, A49, CARD_1:11;
then card ((A1 /\ A2) \/ (A3 /\ A4)) in succ k by ORDINAL1:22;
then ( card ((A1 /\ A2) \/ (A3 /\ A4)) in k or card ((A1 /\ A2) \/ (A3 /\ A4)) = k ) by ORDINAL1:8;
then ( card ((A1 /\ A2) \/ (A3 /\ A4)) in succ (k - 1) or card ((A1 /\ A2) \/ (A3 /\ A4)) = k ) by A25, A57, NAT_1:38;
then A58: ( card ((A1 /\ A2) \/ (A3 /\ A4)) c= k - 1 or card ((A1 /\ A2) \/ (A3 /\ A4)) = k ) by A25, ORDINAL1:22;
A59: card A1 = (k - 1) + 1 by A29;
assume A60: not A6 on L2 ; :: thesis:
A61: ( 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, A31, A32, INCSP_1:1;
hence contradiction by A5, A7, A18, A51, A60, INCSP_1:def 10; :: thesis:

end;

then k + 1 c= card (A1 \/ A2) by A29, A23, Th1;
then card (A1 \/ A2) = (k - 1) + (2 * 1) by A54, XBOOLE_0:def 10;
then A62: card (A1 /\ A2) = k - 1 by A23, A25, A59, Th2;
k + 1 c= card (A3 \/ A4) by A43, A39, A61, Th1;
then card (A3 \/ A4) = (k - 1) + (2 * 1) by A56, XBOOLE_0:def 10;
then A63: card (A3 /\ A4) = k - 1 by A39, A25, A57, Th2;
A64: not card ((A1 /\ A2) \/ (A3 /\ A4)) = k - 1

proof

A65: A5 c= L1 /\ L2 by A21, XBOOLE_1:19;
A66: (A1 /\ A2) /\ (A3 /\ A4) c= A1 /\ A2 by XBOOLE_1:17;
A67: ((A1 /\ A2) /\ A3) /\ A4 = (A1 /\ A2) /\ (A3 /\ A4) by XBOOLE_1:16;
A68: A1 /\ A2 c= A1 by XBOOLE_1:17;
then A69: A1 = (((A1 /\ A2) /\ A3) /\ A4) \/ (A1 \ (((A1 /\ A2) /\ A3) /\ A4)) by A66, A67, XBOOLE_1:1, XBOOLE_1:45;
assume A70: card ((A1 /\ A2) \/ (A3 /\ A4)) = k - 1 ; :: thesis:
then card ((A1 /\ A2) \/ (A3 /\ A4)) = (k - 1) + (2 * 0) ;
then A71: card ((A1 /\ A2) /\ (A3 /\ A4)) = k - 1 by A25, A62, A63, Th2;
then A72: (A1 /\ A2) /\ (A3 /\ A4) = (A1 /\ A2) \/ (A3 /\ A4) by A30, A44, A70, CARD_FIN:1, XBOOLE_1:29;
then card (A1 \ (((A1 /\ A2) /\ A3) /\ A4)) = k - (k - 1) by A29, A30, A70, A68, A66, A67, CARD_2:44, XBOOLE_1:1;
then consider x1 being set such that
A73: A1 \ (((A1 /\ A2) /\ A3) /\ A4) = {x1} by CARD_2:42;
A74: A1 /\ A2 c= A2 by XBOOLE_1:17;
then A75: A2 = (((A1 /\ A2) /\ A3) /\ A4) \/ (A2 \ (((A1 /\ A2) /\ A3) /\ A4)) by A66, A67, XBOOLE_1:1, XBOOLE_1:45;
card (A2 \ (((A1 /\ A2) /\ A3) /\ A4)) = k - (k - 1) by A23, A24, A70, A74, A66, A72, A67, CARD_2:44, XBOOLE_1:1;
then consider x2 being set such that
A76: A2 \ (((A1 /\ A2) /\ A3) /\ A4) = {x2} by CARD_2:42;
x1 in {x1} by TARSKI:def 1;
then A77: not x1 in ((A1 /\ A2) /\ A3) /\ A4 by A73, XBOOLE_0:def 5;
A78: (A1 /\ A2) /\ (A3 /\ A4) c= A3 /\ A4 by XBOOLE_1:17;
A79: A3 /\ A4 c= A4 by XBOOLE_1:17;
then A80: A4 = (((A1 /\ A2) /\ A3) /\ A4) \/ (A4 \ (((A1 /\ A2) /\ A3) /\ A4)) by A78, A67, XBOOLE_1:1, XBOOLE_1:45;
card (A4 \ (((A1 /\ A2) /\ A3) /\ A4)) = k - (k - 1) by A39, A40, A70, A79, A78, A72, A67, CARD_2:44, XBOOLE_1:1;
then consider x4 being set such that
A81: A4 \ (((A1 /\ A2) /\ A3) /\ A4) = {x4} by CARD_2:42;
A82: A3 /\ A4 c= A3 by XBOOLE_1:17;
then A83: A3 = (((A1 /\ A2) /\ A3) /\ A4) \/ (A3 \ (((A1 /\ A2) /\ A3) /\ A4)) by A78, A67, XBOOLE_1:1, XBOOLE_1:45;
card (A3 \ (((A1 /\ A2) /\ A3) /\ A4)) = k - (k - 1) by A43, A44, A70, A82, A78, A72, A67, CARD_2:44, XBOOLE_1:1;
then consider x3 being set such that
A84: A3 \ (((A1 /\ A2) /\ A3) /\ A4) = {x3} by CARD_2:42;
( k + 1 c= card (A3 \/ A4) & card (A3 \/ A4) c= k + 1 ) by A43, A39, A37, A61, A55, Th1, CARD_1:11;
then card (A3 \/ A4) = k + 1 by XBOOLE_0:def 10;
then A3 \/ A4 = L2 by A37, A20, A38, CARD_FIN:1, XBOOLE_1:8;
then A85: L2 = (((A1 /\ A2) /\ A3) /\ A4) \/ ({x3} \/ {x4}) by A84, A81, A83, A80, XBOOLE_1:5;
then A86: L2 = (((A1 /\ A2) /\ A3) /\ A4) \/ {x3,x4} by ENUMSET1:1;
A87: ( 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, A73, A76, A84, A81, A69, A75, A83, A80, 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 A88: not x2 in ((A1 /\ A2) /\ A3) /\ A4 by A76, XBOOLE_0:def 5;
( k + 1 c= card (A1 \/ A2) & card (A1 \/ A2) c= k + 1 ) by A29, A23, A41, A61, A53, Th1, CARD_1:11;
then card (A1 \/ A2) = k + 1 by XBOOLE_0:def 10;
then A1 \/ A2 = L1 by A41, A19, A42, CARD_FIN:1, XBOOLE_1:8;
then A89: L1 = (((A1 /\ A2) /\ A3) /\ A4) \/ ({x1} \/ {x2}) by A73, A76, A69, A75, XBOOLE_1:5;
then A90: L1 = (((A1 /\ A2) /\ A3) /\ A4) \/ {x1,x2} by ENUMSET1:1;
A91: L1 /\ L2 c= ((A1 /\ A2) /\ A3) /\ A4

proof

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

end;

A95: ((A1 /\ A2) /\ A3) /\ A4 c= L2 by A85, XBOOLE_1:10;
((A1 /\ A2) /\ A3) /\ A4 c= L1 by A89, XBOOLE_1:10;
then ((A1 /\ A2) /\ A3) /\ A4 c= L1 /\ L2 by A95, XBOOLE_1:19;
then L1 /\ L2 = ((A1 /\ A2) /\ A3) /\ A4 by A91, XBOOLE_0:def 10;
then card k c= card (k - 1) by A22, A71, A67, A65, CARD_1:11;
then A96: k <= k - 1 by A25, NAT_1:40;
k - 1 <= (k - 1) + 1 by A25, NAT_1:11;
then k = k - 1 by A96, XXREAL_0:1;
hence contradiction ; :: thesis:

end;

k - 1 c= card ((A1 /\ A2) \/ (A3 /\ A4)) by A62, CARD_1:11, XBOOLE_1:7;
then card ((A1 /\ A2) \/ (A3 /\ A4)) = k by A58, A64, XBOOLE_0:def 10;
hence A6 = (A1 /\ A2) \/ (A3 /\ A4) by A33, A34, A48, A46, CARD_FIN:1, XBOOLE_1:8; :: thesis:

end;

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

proof

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

proof

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

end;

A3 = A6

proof

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

end;

hence A6 = (A1 /\ A2) \/ (A3 /\ A4) by A47, A36, A98, XBOOLE_1:12, XBOOLE_1:27; :: thesis:

end;

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

end;

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

proof

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

proof

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

end;

A2 = A6

proof

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

end;

hence A6 = (A1 /\ A2) \/ (A3 /\ A4) by A45, A36, A102, 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 A31, A32, A50; :: thesis: