let k be Element of NAT ; 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 ; ( 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 )
; 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)); INCPROJ:def 8 for b1, b2, b3, b4 being Element of the Lines of (G_ (k,X)) holds
( not A1 on b1 or not A2 on b1 or not A3 on b2 or not A4 on b2 or not A5 on b1 or not A5 on b2 or not A1 on b3 or not A3 on b3 or not A2 on b4 or not A4 on b4 or A5 on b3 or A5 on b4 or b1 = b2 or ex b5 being Element of the Points of (G_ (k,X)) st
( b5 on b3 & b5 on b4 ) )
let L1, L2, L3, L4 be LINE of (G_ (k,X)); ( 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 b1 being Element of the Points of (G_ (k,X)) st
( b1 on L3 & b1 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
; ex b1 being Element of the Points of (G_ (k,X)) st
( b1 on L3 & b1 on L4 )
A15:
( A2 c= L1 & A4 c= L2 )
by A2, A5, A7, Th10;
A16:
( A1 <> A3 & A2 <> A4 )
proof
assume
(
A1 = A3 or
A2 = A4 )
;
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;
verum
end;
A17:
the Lines of (G_ (k,X)) = { L where L is Subset of X : card L = k + 1 }
by A2, Def1;
( 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
; ( 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; verum