let T be _Tree; for X being finite set st ( for x being set st x in X holds
ex t being _Subtree of T st x = the_Vertices_of t ) holds
X is with_Helly_property
let X be finite set ; ( ( for x being set st x in X holds
ex t being _Subtree of T st x = the_Vertices_of t ) implies X is with_Helly_property )
assume A1:
for x being set st x in X holds
ex t being _Subtree of T st x = the_Vertices_of t
; X is with_Helly_property
defpred S1[ Nat] means for H being non empty finite set st card H = $1 & H c= X & ( for x, y being set st x in H & y in H holds
x meets y ) holds
meet H <> {} ;
A2:
for k being Nat st ( for n being Nat st n < k holds
S1[n] ) holds
S1[k]
proof
let k be
Nat;
( ( for n being Nat st n < k holds
S1[n] ) implies S1[k] )
assume A3:
for
n being
Nat st
n < k holds
S1[
n]
;
S1[k]
let H be non
empty finite set ;
( card H = k & H c= X & ( for x, y being set st x in H & y in H holds
x meets y ) implies meet H <> {} )
assume that A4:
card H = k
and A5:
H c= X
and A6:
for
x,
y being
set st
x in H &
y in H holds
x meets y
;
meet H <> {}
per cases
( k = 0 or k = 1 or k > 1 )
by NAT_1:25;
suppose A8:
k > 1
;
meet H <> {} set cH = the
Element of
H;
set A =
H \ { the Element of H};
A9:
card (H \ { the Element of H}) =
(card H) - (card { the Element of H})
by EULER_1:4
.=
k - 1
by A4, CARD_1:30
;
k - 1
> 1
- 1
by A8, XREAL_1:9;
then reconsider A =
H \ { the Element of H} as non
empty finite set by A9;
A10:
A c= X
by A5;
for
x,
y being
set st
x in A &
y in A holds
x meets y
by A6;
then reconsider mA =
meet A as non
empty set by A3, A9, A10, XREAL_1:44;
set cA = the
Element of
A;
set B =
H \ { the Element of A};
A11:
the
Element of
A in A
;
then A12:
card (H \ { the Element of A}) =
(card H) - (card { the Element of A})
by EULER_1:4
.=
k - 1
by A4, CARD_1:30
;
set C =
{ the Element of H, the Element of A};
A13:
meet { the Element of H, the Element of A} = the
Element of
H /\ the
Element of
A
by SETFAM_1:11;
the
Element of
H meets the
Element of
A
by A6, A11;
then reconsider mC =
meet { the Element of H, the Element of A} as non
empty set by A13;
k - 1
> 1
- 1
by A8, XREAL_1:9;
then reconsider B =
H \ { the Element of A} as non
empty finite set by A12;
A14:
B c= X
by A5;
for
x,
y being
set st
x in B &
y in B holds
x meets y
by A6;
then reconsider mB =
meet B as non
empty set by A3, A12, A14, XREAL_1:44;
set a = the
Element of
mA;
set b = the
Element of
mB;
set c = the
Element of
mC;
( the
Element of
mC in mC &
mC c= union { the Element of H, the Element of A} )
by SETFAM_1:2;
then consider cc being
set such that A15:
the
Element of
mC in cc
and A16:
cc in { the Element of H, the Element of A}
by TARSKI:def 4;
the
Element of
H in H
;
then
{ the Element of H, the Element of A} c= X
by A5, A11, A10, ZFMISC_1:32;
then A17:
ex
cct being
_Subtree of
T st
cc = the_Vertices_of cct
by A1, A16;
( the
Element of
mA in mA &
mA c= union A )
by SETFAM_1:2;
then consider aa being
set such that A18:
the
Element of
mA in aa
and A19:
aa in A
by TARSKI:def 4;
( the
Element of
mB in mB &
mB c= union B )
by SETFAM_1:2;
then consider bb being
set such that A20:
the
Element of
mB in bb
and A21:
bb in B
by TARSKI:def 4;
A22:
ex
bbt being
_Subtree of
T st
bb = the_Vertices_of bbt
by A1, A14, A21;
ex
aat being
_Subtree of
T st
aa = the_Vertices_of aat
by A1, A10, A19;
then reconsider a = the
Element of
mA,
b = the
Element of
mB,
c = the
Element of
mC as
Vertex of
T by A18, A20, A22, A15, A17;
A23:
the
Element of
A <> the
Element of
H
by ZFMISC_1:56;
hence
meet H <> {}
by Th53;
verum end; end;
end;
A26:
for n being Nat holds S1[n]
from NAT_1:sch 4(A2);
let H be non empty set ; HELLY:def 4 ( H c= X & ( for x, y being set st x in H & y in H holds
x meets y ) implies meet H <> {} )
assume that
A27:
H c= X
and
A28:
for x, y being set st x in H & y in H holds
x meets y
; meet H <> {}
reconsider H9 = H as finite set by A27;
card H9 = card H9
;
hence
meet H <> {}
by A26, A27, A28; verum