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 )

k <= k + 1 by NAT_1:11;

then A1: Segm k c= Segm (k + 1) by NAT_1:39;

assume A2: ( 0 < k & k + 1 c= card X ) ; :: thesis: G_ (k,X) is Vebleian

then A3: the Points of (G_ (k,X)) = { A where A is Subset of X : card A = k } by Def1;

let A1, A2, A3, A4, A5, A6 be POINT of (G_ (k,X)); :: according to INCPROJ:def 8 :: thesis: for b_{1}, b_{2}, b_{3}, b_{4} being Element of the Lines of (G_ (k,X)) holds

( not A1 on b_{1} or not A2 on b_{1} or not A3 on b_{2} or not A4 on b_{2} or not A5 on b_{1} or not A5 on b_{2} or not A1 on b_{3} or not A3 on b_{3} or not A2 on b_{4} or not A4 on b_{4} or A5 on b_{3} or A5 on b_{4} or b_{1} = b_{2} or ex b_{5} being Element of the Points of (G_ (k,X)) st

( b_{5} on b_{3} & b_{5} on b_{4} ) )

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_{1} being Element of the Points of (G_ (k,X)) st

( b_{1} on L3 & b_{1} on L4 ) )

assume that

A4: A1 on L1 and

A5: A2 on L1 and

A6: A3 on L2 and

A7: A4 on L2 and

A8: ( A5 on L1 & A5 on L2 ) and

A9: A1 on L3 and

A10: A3 on L3 and

A11: A2 on L4 and

A12: A4 on L4 and

A13: ( not A5 on L3 & not A5 on L4 ) and

A14: L1 <> L2 ; :: thesis: ex b_{1} being Element of the Points of (G_ (k,X)) st

( b_{1} on L3 & b_{1} on L4 )

A15: ( A2 c= L1 & A4 c= L2 ) by A2, A5, A7, Th10;

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

( A5 c= L1 & A5 c= L2 ) by A2, A8, Th10;

then A18: A5 c= L1 /\ L2 by XBOOLE_1:19;

A5 in the Points of (G_ (k,X)) ;

then ex B5 being Subset of X st

( B5 = A5 & card B5 = k ) by A3;

then A19: k c= card (L1 /\ L2) by A18, CARD_1:11;

L2 in the Lines of (G_ (k,X)) ;

then A20: ex K2 being Subset of X st

( K2 = L2 & card K2 = k + 1 ) by A17;

A3 in the Points of (G_ (k,X)) ;

then A21: ex B3 being Subset of X st

( B3 = A3 & card B3 = k ) by A3;

A1 in the Points of (G_ (k,X)) ;

then ex B1 being Subset of X st

( B1 = A1 & card B1 = k ) by A3;

then A22: k + 1 c= card (A1 \/ A3) by A21, A16, Th1;

A23: ( A1 c= L1 & A3 c= L2 ) by A2, A4, A6, Th10;

L3 in the Lines of (G_ (k,X)) ;

then A24: ex K3 being Subset of X st

( K3 = L3 & card K3 = k + 1 ) by A17;

then A25: L3 is finite ;

A4 in the Points of (G_ (k,X)) ;

then A26: ex B4 being Subset of X st

( B4 = A4 & card B4 = k ) by A3;

A2 in the Points of (G_ (k,X)) ;

then ex B2 being Subset of X st

( B2 = A2 & card B2 = k ) by A3;

then A27: k + 1 c= card (A2 \/ A4) by A26, A16, Th1;

L4 in the Lines of (G_ (k,X)) ;

then A28: ex K4 being Subset of X st

( K4 = L4 & card K4 = k + 1 ) by A17;

then A29: L4 is finite ;

A30: ( A2 c= L4 & A4 c= L4 ) by A2, A11, A12, Th10;

then A2 \/ A4 c= L4 by XBOOLE_1:8;

then card (A2 \/ A4) c= k + 1 by A28, CARD_1:11;

then card (A2 \/ A4) = k + 1 by A27, XBOOLE_0:def 10;

then A2 \/ A4 = L4 by A28, A30, A29, CARD_2:102, XBOOLE_1:8;

then A31: L4 c= L1 \/ L2 by A15, XBOOLE_1:13;

L1 in the Lines of (G_ (k,X)) ;

then A32: ex K1 being Subset of X st

( K1 = L1 & card K1 = k + 1 ) by A17;

then card (L1 /\ L2) in Segm (k + 1) by A20, A14, Th1;

then card (L1 /\ L2) in succ (Segm k) by NAT_1:38;

then card (L1 /\ L2) c= k by ORDINAL1:22;

then card (L1 /\ L2) = k by A19, XBOOLE_0:def 10;

then A33: card (L1 \/ L2) = k + (2 * 1) by A32, A20, Th2;

A34: ( A1 c= L3 & A3 c= L3 ) by A2, A9, A10, Th10;

then A1 \/ A3 c= L3 by XBOOLE_1:8;

then card (A1 \/ A3) c= k + 1 by A24, CARD_1:11;

then card (A1 \/ A3) = k + 1 by A22, XBOOLE_0:def 10;

then A1 \/ A3 = L3 by A24, A34, A25, CARD_2:102, XBOOLE_1:8;

then L3 c= L1 \/ L2 by A23, XBOOLE_1:13;

then L3 \/ L4 c= L1 \/ L2 by A31, XBOOLE_1:8;

then card (L3 \/ L4) c= k + 2 by A33, CARD_1:11;

then card (L3 \/ L4) in succ (k + 2) by ORDINAL1:22;

then ( card (L3 \/ L4) in Segm ((k + 1) + 1) or card (L3 \/ L4) = k + 2 ) by ORDINAL1:8;

then ( card (L3 \/ L4) in succ (Segm (k + 1)) or card (L3 \/ L4) = k + 2 ) by NAT_1:38;

then A35: ( card (L3 \/ L4) c= k + 1 or card (L3 \/ L4) = k + 2 ) by ORDINAL1:22;

k + 1 c= card (L3 \/ L4) by A24, CARD_1:11, XBOOLE_1:7;

then ( card (L3 \/ L4) = (k + 1) + (2 * 0) or card (L3 \/ L4) = k + (2 * 1) ) by A35, XBOOLE_0:def 10;

then k c= card (L3 /\ L4) by A24, A28, A1, Th2;

then consider B6 being set such that

A36: B6 c= L3 /\ L4 and

A37: card B6 = k by CARD_FIL:36;

A38: L3 /\ L4 c= L3 by XBOOLE_1:17;

then L3 /\ L4 c= X by A24, XBOOLE_1:1;

then reconsider A6 = B6 as Subset of X by A36, XBOOLE_1:1;

A39: A6 in the Points of (G_ (k,X)) by A3, A37;

L3 /\ L4 c= L4 by XBOOLE_1:17;

then A40: B6 c= L4 by A36;

reconsider A6 = A6 as POINT of (G_ (k,X)) by A39;

take B6 ; :: thesis: ( B6 is Element of the Points of (G_ (k,X)) & B6 on L3 & B6 on L4 )

( A6 c= B6 & B6 c= L3 ) by A36, A38;

hence ( B6 is Element of the Points of (G_ (k,X)) & B6 on L3 & B6 on L4 ) by A2, A40, Th10; :: thesis: verum

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 )

k <= k + 1 by NAT_1:11;

then A1: Segm k c= Segm (k + 1) by NAT_1:39;

assume A2: ( 0 < k & k + 1 c= card X ) ; :: thesis: G_ (k,X) is Vebleian

then A3: the Points of (G_ (k,X)) = { A where A is Subset of X : card A = k } by Def1;

let A1, A2, A3, A4, A5, A6 be POINT of (G_ (k,X)); :: according to INCPROJ:def 8 :: thesis: for b

( not A1 on b

( 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

( b

assume that

A4: A1 on L1 and

A5: A2 on L1 and

A6: A3 on L2 and

A7: A4 on L2 and

A8: ( A5 on L1 & A5 on L2 ) and

A9: A1 on L3 and

A10: A3 on L3 and

A11: A2 on L4 and

A12: A4 on L4 and

A13: ( not A5 on L3 & not A5 on L4 ) and

A14: L1 <> L2 ; :: thesis: ex b

( b

A15: ( A2 c= L1 & A4 c= L2 ) by A2, A5, A7, Th10;

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

proof

A17:
the Lines of (G_ (k,X)) = { L where L is Subset of X : card L = k + 1 }
by A2, Def1;
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 A4, A5, A6, A7, A8, INCSP_1:1;

hence contradiction by A9, A11, A13, A14, INCSP_1:def 10; :: thesis: verum

end;then ( ( {A1,A5} on L1 & {A1,A5} on L2 ) or ( {A2,A5} on L1 & {A2,A5} on L2 ) ) by A4, A5, A6, A7, A8, INCSP_1:1;

hence contradiction by A9, A11, A13, A14, INCSP_1:def 10; :: thesis: verum

( A5 c= L1 & A5 c= L2 ) by A2, A8, Th10;

then A18: A5 c= L1 /\ L2 by XBOOLE_1:19;

A5 in the Points of (G_ (k,X)) ;

then ex B5 being Subset of X st

( B5 = A5 & card B5 = k ) by A3;

then A19: k c= card (L1 /\ L2) by A18, CARD_1:11;

L2 in the Lines of (G_ (k,X)) ;

then A20: ex K2 being Subset of X st

( K2 = L2 & card K2 = k + 1 ) by A17;

A3 in the Points of (G_ (k,X)) ;

then A21: ex B3 being Subset of X st

( B3 = A3 & card B3 = k ) by A3;

A1 in the Points of (G_ (k,X)) ;

then ex B1 being Subset of X st

( B1 = A1 & card B1 = k ) by A3;

then A22: k + 1 c= card (A1 \/ A3) by A21, A16, Th1;

A23: ( A1 c= L1 & A3 c= L2 ) by A2, A4, A6, Th10;

L3 in the Lines of (G_ (k,X)) ;

then A24: ex K3 being Subset of X st

( K3 = L3 & card K3 = k + 1 ) by A17;

then A25: L3 is finite ;

A4 in the Points of (G_ (k,X)) ;

then A26: ex B4 being Subset of X st

( B4 = A4 & card B4 = k ) by A3;

A2 in the Points of (G_ (k,X)) ;

then ex B2 being Subset of X st

( B2 = A2 & card B2 = k ) by A3;

then A27: k + 1 c= card (A2 \/ A4) by A26, A16, Th1;

L4 in the Lines of (G_ (k,X)) ;

then A28: ex K4 being Subset of X st

( K4 = L4 & card K4 = k + 1 ) by A17;

then A29: L4 is finite ;

A30: ( A2 c= L4 & A4 c= L4 ) by A2, A11, A12, Th10;

then A2 \/ A4 c= L4 by XBOOLE_1:8;

then card (A2 \/ A4) c= k + 1 by A28, CARD_1:11;

then card (A2 \/ A4) = k + 1 by A27, XBOOLE_0:def 10;

then A2 \/ A4 = L4 by A28, A30, A29, CARD_2:102, XBOOLE_1:8;

then A31: L4 c= L1 \/ L2 by A15, XBOOLE_1:13;

L1 in the Lines of (G_ (k,X)) ;

then A32: ex K1 being Subset of X st

( K1 = L1 & card K1 = k + 1 ) by A17;

then card (L1 /\ L2) in Segm (k + 1) by A20, A14, Th1;

then card (L1 /\ L2) in succ (Segm k) by NAT_1:38;

then card (L1 /\ L2) c= k by ORDINAL1:22;

then card (L1 /\ L2) = k by A19, XBOOLE_0:def 10;

then A33: card (L1 \/ L2) = k + (2 * 1) by A32, A20, Th2;

A34: ( A1 c= L3 & A3 c= L3 ) by A2, A9, A10, Th10;

then A1 \/ A3 c= L3 by XBOOLE_1:8;

then card (A1 \/ A3) c= k + 1 by A24, CARD_1:11;

then card (A1 \/ A3) = k + 1 by A22, XBOOLE_0:def 10;

then A1 \/ A3 = L3 by A24, A34, A25, CARD_2:102, XBOOLE_1:8;

then L3 c= L1 \/ L2 by A23, XBOOLE_1:13;

then L3 \/ L4 c= L1 \/ L2 by A31, XBOOLE_1:8;

then card (L3 \/ L4) c= k + 2 by A33, CARD_1:11;

then card (L3 \/ L4) in succ (k + 2) by ORDINAL1:22;

then ( card (L3 \/ L4) in Segm ((k + 1) + 1) or card (L3 \/ L4) = k + 2 ) by ORDINAL1:8;

then ( card (L3 \/ L4) in succ (Segm (k + 1)) or card (L3 \/ L4) = k + 2 ) by NAT_1:38;

then A35: ( card (L3 \/ L4) c= k + 1 or card (L3 \/ L4) = k + 2 ) by ORDINAL1:22;

k + 1 c= card (L3 \/ L4) by A24, CARD_1:11, XBOOLE_1:7;

then ( card (L3 \/ L4) = (k + 1) + (2 * 0) or card (L3 \/ L4) = k + (2 * 1) ) by A35, XBOOLE_0:def 10;

then k c= card (L3 /\ L4) by A24, A28, A1, Th2;

then consider B6 being set such that

A36: B6 c= L3 /\ L4 and

A37: card B6 = k by CARD_FIL:36;

A38: L3 /\ L4 c= L3 by XBOOLE_1:17;

then L3 /\ L4 c= X by A24, XBOOLE_1:1;

then reconsider A6 = B6 as Subset of X by A36, XBOOLE_1:1;

A39: A6 in the Points of (G_ (k,X)) by A3, A37;

L3 /\ L4 c= L4 by XBOOLE_1:17;

then A40: B6 c= L4 by A36;

reconsider A6 = A6 as POINT of (G_ (k,X)) by A39;

take B6 ; :: thesis: ( B6 is Element of the Points of (G_ (k,X)) & B6 on L3 & B6 on L4 )

( A6 c= B6 & B6 c= L3 ) by A36, A38;

hence ( B6 is Element of the Points of (G_ (k,X)) & B6 on L3 & B6 on L4 ) by A2, A40, Th10; :: thesis: verum