let k be Element of NAT ; :: thesis:
let X be non empty set ; :: thesis:
assume A1: ( 0 < k & k + 1 c= card X ) ; :: thesis:
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:
A2: the Points of (G_ k,X) = { A where A is Subset of X : card A = k } by A1, Def1;
A3: the Lines of (G_ k,X) = { L where L is Subset of X : card L = k + 1 } by A1, Def1;
A1 in the Points of (G_ k,X) ;
then consider B1 being Subset of X such that
A4: ( B1 = A1 & card B1 = k ) by A2;
A2 in the Points of (G_ k,X) ;
then consider B2 being Subset of X such that
A5: ( B2 = A2 & card B2 = k ) by A2;
A3 in the Points of (G_ k,X) ;
then consider B3 being Subset of X such that
A6: ( B3 = A3 & card B3 = k ) by A2;
A4 in the Points of (G_ k,X) ;
then consider B4 being Subset of X such that
A7: ( B4 = A4 & card B4 = k ) by A2;
A5 in the Points of (G_ k,X) ;
then consider B5 being Subset of X such that
A8: ( B5 = A5 & card B5 = k ) by A2;
L1 in the Lines of (G_ k,X) ;
then consider K1 being Subset of X such that
A9: ( K1 = L1 & card K1 = k + 1 ) by A3;
L2 in the Lines of (G_ k,X) ;
then consider K2 being Subset of X such that
A10: ( K2 = L2 & card K2 = k + 1 ) by A3;
L3 in the Lines of (G_ k,X) ;
then consider K3 being Subset of X such that
A11: ( K3 = L3 & card K3 = k + 1 ) by A3;
L4 in the Lines of (G_ k,X) ;
then consider K4 being Subset of X such that
A12: ( K4 = L4 & card K4 = k + 1 ) by A3;
assume A13: ( A1 on L1 & A2 on L1 & A3 on L2 & A4 on L2 & A5 on L1 & A5 on L2 & A1 on L3 & A3 on L3 & A2 on L4 & A4 on L4 & not A5 on L3 & not A5 on L4 & L1 <> L2 & L3 <> L4 ) ; :: thesis:
then A14: ( A1 c= L1 & A2 c= L1 & A3 c= L2 & A4 c= L2 & A5 c= L1 & A5 c= L2 & A1 c= L3 & A3 c= L3 & A2 c= L4 & A4 c= L4 & not A5 c= L3 & not A5 c= L4 ) by A1, Th10;
G_ k,X is Vebleian by A1, Th11;
then consider A6 being POINT of (G_ k,X) such that
A15: ( A6 on L3 & A6 on L4 ) by A13, INCPROJ:def 13;
A6 in the Points of (G_ k,X) ;
then consider a6 being Subset of X such that
A16: ( a6 = A6 & card a6 = k ) by A2;
A17: ( A6 c= L3 & A6 c= L4 & k - 1 is Element of NAT ) by A1, A15, Th10, NAT_1:20;
A19: ( L1 is finite & L2 is finite & L3 is finite & L4 is finite & A6 is finite & A1 is finite & A2 is finite & A3 is finite & A4 is finite ) by A4, A5, A6, A7, A9, A10, A11, A12, A16;
A20: L3 /\ L4 = A6

A21: ( A6 c= L3 /\ L4 & L3 /\ L4 is finite ) by A17, A19, XBOOLE_1:19;
then A22: k c= card (L3 /\ L4) by A16, CARD_1:27;
card (L3 /\ L4) in k + 1 by A11, A12, A13, Th1;
then card (L3 /\ L4) in succ k by NAT_1:39;
then card (L3 /\ L4) c= k by ORDINAL1:34;
then card (L3 /\ L4) = k by A22, XBOOLE_0:def 10;
hence L3 /\ L4 = A6 by A16, A21, CARD_FIN:1; :: thesis:

end;

then A23: ( A1 /\ A2 c= A6 & A3 /\ A4 c= A6 ) by A14, XBOOLE_1:27;
then A24: (A1 /\ A2) \/ (A3 /\ A4) c= A6 by XBOOLE_1:8;
A25: ( (A1 /\ A2) \/ (A3 /\ A4) is finite & A1 /\ A2 c= (A1 /\ A2) \/ (A3 /\ A4) & A3 /\ A4 c= (A1 /\ A2) \/ (A3 /\ A4) ) by A19, XBOOLE_1:7;
A26: ( A6 on L1 implies A6 = (A1 /\ A2) \/ (A3 /\ A4) )

assume A27: A6 on L1 ; :: thesis:
A28: A2 = A6

assume A29: A2 <> A6 ; :: thesis:
( {A2,A6} on L1 & {A2,A6} on L4 ) by A13, A15, A27, INCSP_1:11;
hence contradiction by A13, A29, INCSP_1:def 10; :: thesis:

end;

A1 = A6

assume A30: A1 <> A6 ; :: thesis:
( {A1,A6} on L1 & {A1,A6} on L3 ) by A13, A15, A27, INCSP_1:11;
hence contradiction by A13, A30, INCSP_1:def 10; :: thesis:

end;

hence A6 = (A1 /\ A2) \/ (A3 /\ A4) by A14, A20, A28, XBOOLE_1:12, XBOOLE_1:27; :: thesis:

end;

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

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

assume A33: A6 on L2 ; :: thesis:
A34: A3 = A6

assume A35: A3 <> A6 ; :: thesis:
( {A3,A6} on L2 & {A3,A6} on L3 ) by A13, A15, A33, INCSP_1:11;
hence contradiction by A13, A35, INCSP_1:def 10; :: thesis:

end;

A4 = A6

assume A36: A4 <> A6 ; :: thesis:
( {A4,A6} on L2 & {A4,A6} on L4 ) by A13, A15, A33, INCSP_1:11;
hence contradiction by A13, A36, INCSP_1:def 10; :: thesis:

end;

hence A6 = (A1 /\ A2) \/ (A3 /\ A4) by A14, A20, A34, XBOOLE_1:12, XBOOLE_1:27; :: thesis:

end;

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

assume A37: not A6 on L2 ; :: thesis:
card ((A1 /\ A2) \/ (A3 /\ A4)) = k

A38: ( A1 <> A2 & A3 <> A4 )

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 A13, A15, INCSP_1:11;
hence contradiction by A13, A31, A37, INCSP_1:def 10; :: thesis:

end;

A39: ( A1 \/ A2 c= L1 & A3 \/ A4 c= L2 ) by A14, XBOOLE_1:8;
then ( k + 1 c= card (A1 \/ A2) & card (A1 \/ A2) c= k + 1 & k + 1 c= card (A3 \/ A4) & card (A3 \/ A4) c= k + 1 ) by A4, A5, A6, A7, A9, A10, A38, Th1, CARD_1:27;
then A40: ( card (A3 \/ A4) = (k - 1) + (2 * 1) & card A3 = (k - 1) + 1 & card A4 = (k - 1) + 1 & card (A1 \/ A2) = (k - 1) + (2 * 1) & card A1 = (k - 1) + 1 & card A2 = (k - 1) + 1 ) by A4, A5, A6, A7, XBOOLE_0:def 10;
then A41: ( card (A1 /\ A2) = k - 1 & card (A3 /\ A4) = k - 1 ) by A17, Th2;
then A42: ( card ((A1 /\ A2) \/ (A3 /\ A4)) c= k & k - 1 c= card ((A1 /\ A2) \/ (A3 /\ A4)) ) by A16, A24, CARD_1:27, XBOOLE_1:7;
then card ((A1 /\ A2) \/ (A3 /\ A4)) in succ k by ORDINAL1:34;
then ( card ((A1 /\ A2) \/ (A3 /\ A4)) in k or card ((A1 /\ A2) \/ (A3 /\ A4)) = k ) by ORDINAL1:13;
then ( card ((A1 /\ A2) \/ (A3 /\ A4)) in succ (k - 1) or card ((A1 /\ A2) \/ (A3 /\ A4)) = k ) by A17, A40, NAT_1:39;
then A43: ( card ((A1 /\ A2) \/ (A3 /\ A4)) c= k - 1 or card ((A1 /\ A2) \/ (A3 /\ A4)) = k ) by A17, ORDINAL1:34;
not card ((A1 /\ A2) \/ (A3 /\ A4)) = k - 1

assume A44: card ((A1 /\ A2) \/ (A3 /\ A4)) = k - 1 ; :: thesis:
then card ((A1 /\ A2) \/ (A3 /\ A4)) = (k - 1) + (2 * 0 ) ;
then A45: card ((A1 /\ A2) /\ (A3 /\ A4)) = k - 1 by A17, A41, Th2;
then ( (A1 /\ A2) /\ (A3 /\ A4) c= (A1 /\ A2) \/ (A3 /\ A4) & (A1 /\ A2) /\ (A3 /\ A4) is finite ) by A17, XBOOLE_1:29;
then ( (A1 /\ A2) /\ (A3 /\ A4) c= (A1 /\ A2) \/ (A3 /\ A4) & ((A1 /\ A2) /\ A3) /\ A4 is finite & (A1 /\ A2) /\ (A3 /\ A4) is finite & A1 /\ A2 c= A1 & A1 /\ A2 c= A2 & A3 /\ A4 c= A3 & A3 /\ A4 c= A4 & (A1 /\ A2) /\ (A3 /\ A4) c= A1 /\ A2 & (A1 /\ A2) /\ (A3 /\ A4) c= A3 /\ A4 ) by XBOOLE_1:16, XBOOLE_1:17;
then A47: ( (A1 /\ A2) /\ (A3 /\ A4) = (A1 /\ A2) \/ (A3 /\ A4) & (A1 /\ A2) /\ (A3 /\ A4) c= A1 & (A1 /\ A2) /\ (A3 /\ A4) c= A2 & (A1 /\ A2) /\ (A3 /\ A4) c= A3 & (A1 /\ A2) /\ (A3 /\ A4) c= A4 & ((A1 /\ A2) /\ A3) /\ A4 = (A1 /\ A2) /\ (A3 /\ A4) ) by A25, A44, A45, CARD_FIN:1, XBOOLE_1:1, XBOOLE_1:16;
then A48: ( card (A1 \ (((A1 /\ A2) /\ A3) /\ A4)) = k - (k - 1) & card (A2 \ (((A1 /\ A2) /\ A3) /\ A4)) = k - (k - 1) & card (A3 \ (((A1 /\ A2) /\ A3) /\ A4)) = k - (k - 1) & card (A4 \ (((A1 /\ A2) /\ A3) /\ A4)) = k - (k - 1) ) by A4, A5, A6, A7, A19, A44, CARD_2:63;
then consider x1 being set such that
A49: A1 \ (((A1 /\ A2) /\ A3) /\ A4) = {x1} by CARD_2:60;
consider x2 being set such that
A50: A2 \ (((A1 /\ A2) /\ A3) /\ A4) = {x2} by A48, CARD_2:60;
consider x3 being set such that
A51: A3 \ (((A1 /\ A2) /\ A3) /\ A4) = {x3} by A48, CARD_2:60;
consider x4 being set such that
A52: A4 \ (((A1 /\ A2) /\ A3) /\ A4) = {x4} by A48, CARD_2:60;
A53: ( A1 = (((A1 /\ A2) /\ A3) /\ A4) \/ (A1 \ (((A1 /\ A2) /\ A3) /\ A4)) & A2 = (((A1 /\ A2) /\ A3) /\ A4) \/ (A2 \ (((A1 /\ A2) /\ A3) /\ A4)) & A3 = (((A1 /\ A2) /\ A3) /\ A4) \/ (A3 \ (((A1 /\ A2) /\ A3) /\ A4)) & A4 = (((A1 /\ A2) /\ A3) /\ A4) \/ (A4 \ (((A1 /\ A2) /\ A3) /\ A4)) & x1 in A1 \ (((A1 /\ A2) /\ A3) /\ A4) & x2 in A2 \ (((A1 /\ A2) /\ A3) /\ A4) & x3 in A3 \ (((A1 /\ A2) /\ A3) /\ A4) & x4 in A4 \ (((A1 /\ A2) /\ A3) /\ A4) ) by A47, A49, A50, A51, A52, TARSKI:def 1, XBOOLE_1:45;
A54: ( x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 )

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 A13, A49, A50, A51, A52, A53, INCSP_1:11;
hence contradiction by A13, INCSP_1:def 10; :: thesis:

end;

( k + 1 c= card (A1 \/ A2) & k + 1 c= card (A3 \/ A4) & card (A1 \/ A2) c= k + 1 & card (A3 \/ A4) c= k + 1 ) by A4, A5, A6, A7, A9, A10, A38, A39, Th1, CARD_1:27;
then ( A1 \/ A2 is finite & A3 \/ A4 is finite & card (A1 \/ A2) = k + 1 & card (A3 \/ A4) = k + 1 ) by XBOOLE_0:def 10;
then ( A1 \/ A2 = L1 & A3 \/ A4 = L2 ) by A9, A10, A14, A19, CARD_FIN:1, XBOOLE_1:8;
then A55: ( L1 = (((A1 /\ A2) /\ A3) /\ A4) \/ ({x1} \/ {x2}) & L2 = (((A1 /\ A2) /\ A3) /\ A4) \/ ({x3} \/ {x4}) ) by A49, A50, A51, A52, A53, XBOOLE_1:5;
then A56: ( L1 = (((A1 /\ A2) /\ A3) /\ A4) \/ {x1,x2} & L2 = (((A1 /\ A2) /\ A3) /\ A4) \/ {x3,x4} ) by ENUMSET1:41;
( x1 in {x1} & x2 in {x2} & x3 in {x3} & x4 in {x4} ) by TARSKI:def 1;
then A57: ( not x1 in ((A1 /\ A2) /\ A3) /\ A4 & not x2 in ((A1 /\ A2) /\ A3) /\ A4 & not x3 in ((A1 /\ A2) /\ A3) /\ A4 & not x4 in ((A1 /\ A2) /\ A3) /\ A4 ) by A49, A50, A51, A52, XBOOLE_0:def 5;
A58: A5 c= L1 /\ L2 by A14, XBOOLE_1:19;
L1 /\ L2 = ((A1 /\ A2) /\ A3) /\ A4

thus L1 /\ L2 c= ((A1 /\ A2) /\ A3) /\ A4 :: according to XBOOLE_0:def 10 :: thesis:

assume not L1 /\ L2 c= ((A1 /\ A2) /\ A3) /\ A4 ; :: thesis:
then consider x being set such that
A59: ( x in L1 /\ L2 & not x in ((A1 /\ A2) /\ A3) /\ A4 ) by TARSKI:def 3;
A60: ( x in L1 & x in L2 & not x in ((A1 /\ A2) /\ A3) /\ A4 ) by A59, XBOOLE_0:def 4;
then x in {x1,x2} by A56, XBOOLE_0:def 3;
then ( x1 in L2 or x2 in L2 ) by A60, TARSKI:def 2;
then ( x1 in {x3,x4} or x2 in {x3,x4} ) by A56, A57, XBOOLE_0:def 3;
hence contradiction by A54, TARSKI:def 2; :: thesis:

end;

thus ((A1 /\ A2) /\ A3) /\ A4 c= L1 /\ L2 :: thesis:

( ((A1 /\ A2) /\ A3) /\ A4 c= L1 & ((A1 /\ A2) /\ A3) /\ A4 c= L2 ) by A55, XBOOLE_1:10;
hence ((A1 /\ A2) /\ A3) /\ A4 c= L1 /\ L2 by XBOOLE_1:19; :: thesis:

end;

thus verum ; :: thesis:

end;

then ( card k c= card (k - 1) & k - 1 <= (k - 1) + 1 ) by A8, A17, A44, A47, A58, CARD_1:27, NAT_1:11;
then ( k <= k - 1 & k - 1 <= k ) by A17, NAT_1:41;
then k = k - 1 by XXREAL_0:1;
hence contradiction ; :: thesis:

end;

hence card ((A1 /\ A2) \/ (A3 /\ A4)) = k by A42, A43, XBOOLE_0:def 10; :: thesis:

end;

hence A6 = (A1 /\ A2) \/ (A3 /\ A4) by A16, A19, A23, CARD_FIN:1, XBOOLE_1:8; :: thesis:

end;

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

end;

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