let k be Element of NAT ; for X being non empty set st 0 < k & k + 1 c= card X holds
for A1, A2, A3, A4, A5, A6 being POINT of (G_ (k,X))
for L1, L2, L3, L4 being LINE of (G_ (k,X)) st 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 holds
ex A6 being POINT of (G_ (k,X)) st
( A6 on L3 & A6 on L4 & A6 = (A1 /\ A2) \/ (A3 /\ A4) )
let X be non empty set ; ( 0 < k & k + 1 c= card X implies for A1, A2, A3, A4, A5, A6 being POINT of (G_ (k,X))
for L1, L2, L3, L4 being LINE of (G_ (k,X)) st 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 holds
ex A6 being POINT of (G_ (k,X)) st
( A6 on L3 & A6 on L4 & A6 = (A1 /\ A2) \/ (A3 /\ A4) ) )
assume that
A1:
0 < k
and
A2:
k + 1 c= card X
; for A1, A2, A3, A4, A5, A6 being POINT of (G_ (k,X))
for L1, L2, L3, L4 being LINE of (G_ (k,X)) st 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 holds
ex A6 being POINT of (G_ (k,X)) st
( A6 on L3 & A6 on L4 & A6 = (A1 /\ A2) \/ (A3 /\ A4) )
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)); for L1, L2, L3, L4 being LINE of (G_ (k,X)) st 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 holds
ex A6 being POINT of (G_ (k,X)) st
( A6 on L3 & A6 on L4 & A6 = (A1 /\ A2) \/ (A3 /\ A4) )
let L1, L2, L3, L4 be LINE of (G_ (k,X)); ( 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 implies ex A6 being POINT of (G_ (k,X)) st
( A6 on L3 & A6 on L4 & A6 = (A1 /\ A2) \/ (A3 /\ A4) ) )
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
; ex A6 being POINT of (G_ (k,X)) st
( A6 on L3 & A6 on L4 & A6 = (A1 /\ A2) \/ (A3 /\ A4) )
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
;
reconsider k1 = k - 1 as Element of NAT by A1, NAT_1:20;
L3 in the Lines of (G_ (k,X))
;
then A25:
ex K3 being Subset of X st
( K3 = L3 & card K3 = k + 1 )
by A4;
then A26:
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 Segm (k + 1)
by A25, A18, Th1;
then
card (L3 /\ L4) in succ (Segm k)
by NAT_1:38;
then A27:
card (L3 /\ L4) c= k
by ORDINAL1:22;
A1 in the Points of (G_ (k,X))
;
then A28:
ex B1 being Subset of X st
( B1 = A1 & card B1 = k )
by A3;
then A29:
A1 is finite
;
G_ (k,X) is Vebleian
by A1, A2, Th11;
then consider A6 being POINT of (G_ (k,X)) such that
A30:
A6 on L3
and
A31:
A6 on L4
by A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17;
A6 in the Points of (G_ (k,X))
;
then A32:
ex a6 being Subset of X st
( a6 = A6 & card a6 = k )
by A3;
then A33:
A6 is finite
;
A34:
( A6 c= L3 & A6 c= L4 )
by A1, A2, A30, A31, Th10;
then
A6 c= L3 /\ L4
by XBOOLE_1:19;
then
k c= card (L3 /\ L4)
by A32, CARD_1:11;
then
card (L3 /\ L4) = k
by A27, XBOOLE_0:def 10;
then A35:
L3 /\ L4 = A6
by A32, A34, A26, CARD_2:102, XBOOLE_1:19;
L2 in the Lines of (G_ (k,X))
;
then A36:
ex K2 being Subset of X st
( K2 = L2 & card K2 = k + 1 )
by A4;
then A37:
L2 is finite
;
A4 in the Points of (G_ (k,X))
;
then A38:
ex B4 being Subset of X st
( B4 = A4 & card B4 = k )
by A3;
then A39:
A4 is finite
;
L1 in the Lines of (G_ (k,X))
;
then A40:
ex K1 being Subset of X st
( K1 = L1 & card K1 = k + 1 )
by A4;
then A41:
L1 is finite
;
A3 in the Points of (G_ (k,X))
;
then A42:
ex B3 being Subset of X st
( B3 = A3 & card B3 = k )
by A3;
then A43:
A3 is finite
;
A44:
( A3 c= L3 & A4 c= L4 )
by A1, A2, A12, A14, Th10;
then A45:
A3 /\ A4 c= A6
by A35, XBOOLE_1:27;
A46:
( A1 c= L3 & A2 c= L4 )
by A1, A2, A11, A13, Th10;
then A47:
A1 /\ A2 c= A6
by A35, XBOOLE_1:27;
then A48:
(A1 /\ A2) \/ (A3 /\ A4) c= A6
by A45, XBOOLE_1:8;
A49:
( not A6 on L1 implies A6 = (A1 /\ A2) \/ (A3 /\ A4) )
proof
assume A50:
not
A6 on L1
;
A6 = (A1 /\ A2) \/ (A3 /\ A4)
A51:
( not
A6 on L2 implies
A6 = (A1 /\ A2) \/ (A3 /\ A4) )
proof
A52:
A1 \/ A2 c= L1
by A19, XBOOLE_1:8;
then A53:
card (A1 \/ A2) c= k + 1
by A40, CARD_1:11;
A54:
A3 \/ A4 c= L2
by A20, XBOOLE_1:8;
then A55:
card (A3 \/ A4) c= k + 1
by A36, CARD_1:11;
A56:
card A3 = (k - 1) + 1
by A42;
card ((A1 /\ A2) \/ (A3 /\ A4)) c= k
by A32, A48, CARD_1:11;
then
card ((A1 /\ A2) \/ (A3 /\ A4)) in succ k
by ORDINAL1:22;
then
(
card ((A1 /\ A2) \/ (A3 /\ A4)) in Segm (k1 + 1) or
card ((A1 /\ A2) \/ (A3 /\ A4)) = k )
by ORDINAL1:8;
then
(
card ((A1 /\ A2) \/ (A3 /\ A4)) in succ (Segm k1) or
card ((A1 /\ A2) \/ (A3 /\ A4)) = k )
by NAT_1:38;
then A57:
(
card ((A1 /\ A2) \/ (A3 /\ A4)) c= Segm k1 or
card ((A1 /\ A2) \/ (A3 /\ A4)) = k )
by ORDINAL1:22;
A58:
card A1 = (k - 1) + 1
by A28;
assume A59:
not
A6 on L2
;
A6 = (A1 /\ A2) \/ (A3 /\ A4)
A60:
(
A1 <> A2 &
A3 <> A4 )
proof
assume
(
A1 = A2 or
A3 = A4 )
;
contradiction
then
( (
{A1,A6} on L3 &
{A1,A6} on L4 ) or (
{A3,A6} on L3 &
{A3,A6} on L4 ) )
by A11, A12, A13, A14, A30, A31, INCSP_1:1;
hence
contradiction
by A5, A7, A18, A50, A59, INCSP_1:def 10;
verum
end;
then
k + 1
c= card (A1 \/ A2)
by A28, A23, Th1;
then
card (A1 \/ A2) = k1 + (2 * 1)
by A53, XBOOLE_0:def 10;
then A61:
card (A1 /\ A2) = k1
by A23, A58, Th2;
k + 1
c= card (A3 \/ A4)
by A42, A38, A60, Th1;
then
card (A3 \/ A4) = k1 + (2 * 1)
by A55, XBOOLE_0:def 10;
then A62:
card (A3 /\ A4) = k1
by A38, A56, Th2;
A63:
not
card ((A1 /\ A2) \/ (A3 /\ A4)) = k - 1
proof
A64:
A5 c= L1 /\ L2
by A21, XBOOLE_1:19;
A65:
(A1 /\ A2) /\ (A3 /\ A4) c= A1 /\ A2
by XBOOLE_1:17;
A66:
((A1 /\ A2) /\ A3) /\ A4 = (A1 /\ A2) /\ (A3 /\ A4)
by XBOOLE_1:16;
A67:
A1 /\ A2 c= A1
by XBOOLE_1:17;
then A68:
A1 = (((A1 /\ A2) /\ A3) /\ A4) \/ (A1 \ (((A1 /\ A2) /\ A3) /\ A4))
by A65, A66, XBOOLE_1:1, XBOOLE_1:45;
assume A69:
card ((A1 /\ A2) \/ (A3 /\ A4)) = k - 1
;
contradiction
then
card ((A1 /\ A2) \/ (A3 /\ A4)) = k1 + (2 * 0)
;
then A70:
card ((A1 /\ A2) /\ (A3 /\ A4)) = k1
by A61, A62, Th2;
then A71:
(A1 /\ A2) /\ (A3 /\ A4) = (A1 /\ A2) \/ (A3 /\ A4)
by A29, A43, A69, CARD_2:102, XBOOLE_1:29;
then
card (A1 \ (((A1 /\ A2) /\ A3) /\ A4)) = k - (k - 1)
by A28, A29, A69, A67, A65, A66, CARD_2:44, XBOOLE_1:1;
then consider x1 being
object such that A72:
A1 \ (((A1 /\ A2) /\ A3) /\ A4) = {x1}
by CARD_2:42;
A73:
A1 /\ A2 c= A2
by XBOOLE_1:17;
then A74:
A2 = (((A1 /\ A2) /\ A3) /\ A4) \/ (A2 \ (((A1 /\ A2) /\ A3) /\ A4))
by A65, A66, XBOOLE_1:1, XBOOLE_1:45;
card (A2 \ (((A1 /\ A2) /\ A3) /\ A4)) = k - (k - 1)
by A23, A24, A69, A73, A65, A71, A66, CARD_2:44, XBOOLE_1:1;
then consider x2 being
object such that A75:
A2 \ (((A1 /\ A2) /\ A3) /\ A4) = {x2}
by CARD_2:42;
x1 in {x1}
by TARSKI:def 1;
then A76:
not
x1 in ((A1 /\ A2) /\ A3) /\ A4
by A72, XBOOLE_0:def 5;
A77:
(A1 /\ A2) /\ (A3 /\ A4) c= A3 /\ A4
by XBOOLE_1:17;
A78:
A3 /\ A4 c= A4
by XBOOLE_1:17;
then A79:
A4 = (((A1 /\ A2) /\ A3) /\ A4) \/ (A4 \ (((A1 /\ A2) /\ A3) /\ A4))
by A77, A66, XBOOLE_1:1, XBOOLE_1:45;
card (A4 \ (((A1 /\ A2) /\ A3) /\ A4)) = k - (k - 1)
by A38, A39, A69, A78, A77, A71, A66, CARD_2:44, XBOOLE_1:1;
then consider x4 being
object such that A80:
A4 \ (((A1 /\ A2) /\ A3) /\ A4) = {x4}
by CARD_2:42;
A81:
A3 /\ A4 c= A3
by XBOOLE_1:17;
then A82:
A3 = (((A1 /\ A2) /\ A3) /\ A4) \/ (A3 \ (((A1 /\ A2) /\ A3) /\ A4))
by A77, A66, XBOOLE_1:1, XBOOLE_1:45;
card (A3 \ (((A1 /\ A2) /\ A3) /\ A4)) = k - (k - 1)
by A42, A43, A69, A81, A77, A71, A66, CARD_2:44, XBOOLE_1:1;
then consider x3 being
object such that A83:
A3 \ (((A1 /\ A2) /\ A3) /\ A4) = {x3}
by CARD_2:42;
(
k + 1
c= card (A3 \/ A4) &
card (A3 \/ A4) c= k + 1 )
by A42, A38, A36, A60, A54, Th1, CARD_1:11;
then
card (A3 \/ A4) = k + 1
by XBOOLE_0:def 10;
then
A3 \/ A4 = L2
by A36, A20, A37, CARD_2:102, XBOOLE_1:8;
then A84:
L2 = (((A1 /\ A2) /\ A3) /\ A4) \/ ({x3} \/ {x4})
by A83, A80, A82, A79, XBOOLE_1:5;
then A85:
L2 = (((A1 /\ A2) /\ A3) /\ A4) \/ {x3,x4}
by ENUMSET1:1;
A86:
(
x1 <> x3 &
x1 <> x4 &
x2 <> x3 &
x2 <> x4 )
proof
assume
(
x1 = x3 or
x1 = x4 or
x2 = x3 or
x2 = x4 )
;
contradiction
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, A72, A75, A83, A80, A68, A74, A82, A79, INCSP_1:1;
hence
contradiction
by A11, A13, A15, A16, A17, INCSP_1:def 10;
verum
end;
x2 in {x2}
by TARSKI:def 1;
then A87:
not
x2 in ((A1 /\ A2) /\ A3) /\ A4
by A75, XBOOLE_0:def 5;
(
k + 1
c= card (A1 \/ A2) &
card (A1 \/ A2) c= k + 1 )
by A28, A23, A40, A60, A52, Th1, CARD_1:11;
then
card (A1 \/ A2) = k + 1
by XBOOLE_0:def 10;
then
A1 \/ A2 = L1
by A40, A19, A41, CARD_2:102, XBOOLE_1:8;
then A88:
L1 = (((A1 /\ A2) /\ A3) /\ A4) \/ ({x1} \/ {x2})
by A72, A75, A68, A74, XBOOLE_1:5;
then A89:
L1 = (((A1 /\ A2) /\ A3) /\ A4) \/ {x1,x2}
by ENUMSET1:1;
A90:
L1 /\ L2 c= ((A1 /\ A2) /\ A3) /\ A4
proof
assume
not
L1 /\ L2 c= ((A1 /\ A2) /\ A3) /\ A4
;
contradiction
then consider x being
object such that A91:
x in L1 /\ L2
and A92:
not
x in ((A1 /\ A2) /\ A3) /\ A4
;
x in L1
by A91, XBOOLE_0:def 4;
then A93:
x in {x1,x2}
by A89, A92, XBOOLE_0:def 3;
x in L2
by A91, XBOOLE_0:def 4;
then
(
x1 in L2 or
x2 in L2 )
by A93, TARSKI:def 2;
then
(
x1 in {x3,x4} or
x2 in {x3,x4} )
by A85, A76, A87, XBOOLE_0:def 3;
hence
contradiction
by A86, TARSKI:def 2;
verum
end;
A94:
((A1 /\ A2) /\ A3) /\ A4 c= L2
by A84, XBOOLE_1:10;
((A1 /\ A2) /\ A3) /\ A4 c= L1
by A88, XBOOLE_1:10;
then
((A1 /\ A2) /\ A3) /\ A4 c= L1 /\ L2
by A94, XBOOLE_1:19;
then
L1 /\ L2 = ((A1 /\ A2) /\ A3) /\ A4
by A90, XBOOLE_0:def 10;
then
card (Segm k) c= card (Segm k1)
by A22, A70, A66, A64, CARD_1:11;
then A95:
k <= k1
by NAT_1:40;
k1 <= k1 + 1
by NAT_1:11;
then
k = k - 1
by A95, XXREAL_0:1;
hence
contradiction
;
verum
end;
k - 1
c= card ((A1 /\ A2) \/ (A3 /\ A4))
by A61, CARD_1:11, XBOOLE_1:7;
then
card ((A1 /\ A2) \/ (A3 /\ A4)) = k
by A57, A63, XBOOLE_0:def 10;
hence
A6 = (A1 /\ A2) \/ (A3 /\ A4)
by A32, A33, A47, A45, CARD_2:102, XBOOLE_1:8;
verum
end;
(
A6 on L2 implies
A6 = (A1 /\ A2) \/ (A3 /\ A4) )
hence
A6 = (A1 /\ A2) \/ (A3 /\ A4)
by A51;
verum
end;
( A6 on L1 implies A6 = (A1 /\ A2) \/ (A3 /\ A4) )
hence
ex A6 being POINT of (G_ (k,X)) st
( A6 on L3 & A6 on L4 & A6 = (A1 /\ A2) \/ (A3 /\ A4) )
by A30, A31, A49; verum