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 Vebleian
let X be non empty set ; :: thesis: ( 0 < k & k + 1 c= card X implies G_ k,X is Vebleian )
assume A1: ( 0 < k & k + 1 c= card X ) ; :: thesis: G_ k,X is Vebleian
let A1, A2, A3, A4, A5, A6 be POINT of (G_ k,X); :: according to INCPROJ:def 13 :: thesis: for b₁, b₂, b₃, b₄ being Element of the Lines of (G_ k,X) holds
( not A1 on b₁ or not A2 on b₁ or not A3 on b₂ or not A4 on b₂ or not A5 on b₁ or not A5 on b₂ or not A1 on b₃ or not A3 on b₃ or not A2 on b₄ or not A4 on b₄ or A5 on b₃ or A5 on b₄ or b₁ = b₂ or ex b₅ being Element of the Points of (G_ k,X) st
( b₅ on b₃ & b₅ on b₄ ) )
let L1, L2, L3, L4 be LINE of (G_ k,X); :: thesis: ( not A1 on L1 or not A2 on L1 or not A3 on L2 or not A4 on L2 or not A5 on L1 or not A5 on L2 or not A1 on L3 or not A3 on L3 or not A2 on L4 or not A4 on L4 or A5 on L3 or A5 on L4 or L1 = L2 or ex b₁ being Element of the Points of (G_ k,X) st
( b₁ on L3 & b₁ on L4 ) )
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 ) ; :: thesis: ex b₁ being Element of the Points of (G_ k,X) st
( b₁ on L3 & b₁ on L4 )
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;
then A5 c= L1 /\ L2 by XBOOLE_1:19;
then A15: k c= card (L1 /\ L2) by A8, CARD_1:27;
card (L1 /\ L2) in k + 1 by A9, A10, A13, Th1;
then card (L1 /\ L2) in succ k by NAT_1:39;
then card (L1 /\ L2) c= k by ORDINAL1:34;
then card (L1 /\ L2) = k by A15, XBOOLE_0:def 10;
then A16: card (L1 \/ L2) = k + (2 * 1) by A9, A10, Th2;
( A1 \/ A3 c= L3 & A2 \/ A4 c= L4 ) by A14, XBOOLE_1:8;
then A17: ( card (A1 \/ A3) c= k + 1 & card (A2 \/ A4) c= k + 1 ) by A11, A12, CARD_1:27;
( A1 <> A3 & A2 <> A4 )

proof

assume ( A1 = A3 or A2 = A4 ) ; :: thesis: contradiction
then ( ( {A1,A5} on L1 & {A1,A5} on L2 ) or ( {A2,A5} on L1 & {A2,A5} on L2 ) ) by A13, INCSP_1:11;
hence contradiction by A13, INCSP_1:def 10; :: thesis: verum

end;

then ( k + 1 c= card (A1 \/ A3) & k + 1 c= card (A2 \/ A4) ) by A4, A5, A6, A7, Th1;
then A18: ( card (A1 \/ A3) = k + 1 & card (A2 \/ A4) = k + 1 & card (k + 1) = k + 1 ) by A17, CARD_1:def 5, XBOOLE_0:def 10;
then ( A1 \/ A3 is finite & L3 is finite & A2 \/ A4 is finite & L4 is finite ) by A11, A12;
then ( A1 \/ A3 = L3 & A2 \/ A4 = L4 ) by A11, A12, A14, A18, CARD_FIN:1, XBOOLE_1:8;
then ( L3 c= L1 \/ L2 & L4 c= L1 \/ L2 ) by A14, XBOOLE_1:13;
then ( L3 c= L3 \/ L4 & L3 \/ L4 c= L1 \/ L2 ) by XBOOLE_1:7, XBOOLE_1:8;
then A19: ( card (L3 \/ L4) c= k + 2 & k + 1 c= card (L3 \/ L4) ) by A11, A16, CARD_1:27;
k c= card (L3 /\ L4)

proof

card (L3 \/ L4) in succ (k + 2) by A19, ORDINAL1:34;
then ( card (L3 \/ L4) in (k + 1) + 1 or card (L3 \/ L4) = k + 2 ) by ORDINAL1:13;
then ( card (L3 \/ L4) in succ (k + 1) or card (L3 \/ L4) = k + 2 ) by NAT_1:39;
then ( card (L3 \/ L4) c= k + 1 or card (L3 \/ L4) = k + 2 ) by ORDINAL1:34;
then ( card (L3 \/ L4) = (k + 1) + (2 * 0 ) or card (L3 \/ L4) = k + (2 * 1) ) by A19, XBOOLE_0:def 10;
then ( ( k + 1 c= card (L3 /\ L4) or k c= card (L3 /\ L4) ) & k <= k + 1 ) by A11, A12, Th2, NAT_1:11;
then ( ( k + 1 c= card (L3 /\ L4) or k c= card (L3 /\ L4) ) & k c= k + 1 ) by NAT_1:40;
hence k c= card (L3 /\ L4) by XBOOLE_1:1; :: thesis: verum

end;

then consider B6 being set such that
A20: ( B6 c= L3 /\ L4 & card B6 = k ) by CARD_FIL:36;
take B6 ; :: thesis: ( B6 is Element of the Points of (G_ k,X) & B6 on L3 & B6 on L4 )
A21: ( L3 /\ L4 c= L3 & L3 /\ L4 c= L4 & L3 c= X ) by A11, XBOOLE_1:17;
then L3 /\ L4 c= X by XBOOLE_1:1;
then reconsider A6 = B6 as Subset of X by A20, XBOOLE_1:1;
A6 in the Points of (G_ k,X) by A2, A20;
then reconsider A6 = A6 as POINT of (G_ k,X) ;
( A6 c= B6 & B6 c= L3 & B6 c= L4 ) by A20, A21, XBOOLE_1:1;
hence ( B6 is Element of the Points of (G_ k,X) & B6 on L3 & B6 on L4 ) by A1, Th10; :: thesis: verum