let T be _Tree; :: thesis: 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 ; :: thesis: ( ( 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 ; :: thesis: X is with_Helly_property

defpred S_{1}[ 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

S_{1}[n] ) holds

S_{1}[k]
_{1}[n]
from NAT_1:sch 4(A2);

let H be non empty set ; :: according to HELLY:def 4 :: thesis: ( 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 ; :: thesis: meet H <> {}

reconsider H9 = H as finite set by A27;

card H9 = card H9 ;

hence meet H <> {} by A26, A27, A28; :: thesis: verum

ex t being _Subtree of T st x = the_Vertices_of t ) holds

X is with_Helly_property

let X be finite set ; :: thesis: ( ( 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 ; :: thesis: X is with_Helly_property

defpred S

x meets y ) holds

meet H <> {} ;

A2: for k being Nat st ( for n being Nat st n < k holds

S

S

proof

A26:
for n being Nat holds S
let k be Nat; :: thesis: ( ( for n being Nat st n < k holds

S_{1}[n] ) implies S_{1}[k] )

assume A3: for n being Nat st n < k holds

S_{1}[n]
; :: thesis: S_{1}[k]

let H be non empty finite set ; :: thesis: ( 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 ; :: thesis: meet H <> {}

end;S

assume A3: for n being Nat st n < k holds

S

let H be non empty finite set ; :: thesis: ( 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 ; :: thesis: meet H <> {}

per cases
( k = 0 or k = 1 or k > 1 )
by NAT_1:25;

end;

suppose
k = 1
; :: thesis: meet H <> {}

then consider x being Element of H such that

A7: H = {x} by A4, PRE_CIRC:25;

ex t being _Subtree of T st x = the_Vertices_of t by A1, A5;

hence meet H <> {} by A7, SETFAM_1:10; :: thesis: verum

end;A7: H = {x} by A4, PRE_CIRC:25;

ex t being _Subtree of T st x = the_Vertices_of t by A1, A5;

hence meet H <> {} by A7, SETFAM_1:10; :: thesis: verum

suppose A8:
k > 1
; :: thesis: 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;

end;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;

now :: thesis: for s being set st s in H holds

( ex t being _Subtree of T st s = the_Vertices_of t & ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) )

hence
meet H <> {}
by Th53; :: thesis: verum( ex t being _Subtree of T st s = the_Vertices_of t & ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) )

let s be set ; :: thesis: ( s in H implies ( ex t being _Subtree of T st s = the_Vertices_of t & ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) ) )

assume A24: s in H ; :: thesis: ( ex t being _Subtree of T st s = the_Vertices_of t & ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) )

hence ex t being _Subtree of T st s = the_Vertices_of t by A1, A5; :: thesis: ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) )

thus ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) :: thesis: verum

end;assume A24: s in H ; :: thesis: ( ex t being _Subtree of T st s = the_Vertices_of t & ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) )

hence ex t being _Subtree of T st s = the_Vertices_of t by A1, A5; :: thesis: ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) )

thus ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) :: thesis: verum

proof
end;

per cases
( s = the Element of H or s = the Element of A or ( s <> the Element of H & s <> the Element of A ) )
;

end;

suppose
s = the Element of H
; :: thesis: ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) )

then
( s in { the Element of H, the Element of A} & s in B )
by A23, TARSKI:def 2, ZFMISC_1:56;

hence ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) by SETFAM_1:def 1; :: thesis: verum

end;hence ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) by SETFAM_1:def 1; :: thesis: verum

suppose A25:
s = the Element of A
; :: thesis: ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) )

then
s in { the Element of H, the Element of A}
by TARSKI:def 2;

hence ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) by A25, SETFAM_1:def 1; :: thesis: verum

end;hence ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) by A25, SETFAM_1:def 1; :: thesis: verum

suppose
( s <> the Element of H & s <> the Element of A )
; :: thesis: ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) )

then
( s in A & s in B )
by A24, ZFMISC_1:56;

hence ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) by SETFAM_1:def 1; :: thesis: verum

end;hence ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) by SETFAM_1:def 1; :: thesis: verum

let H be non empty set ; :: according to HELLY:def 4 :: thesis: ( 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 ; :: thesis: meet H <> {}

reconsider H9 = H as finite set by A27;

card H9 = card H9 ;

hence meet H <> {} by A26, A27, A28; :: thesis: verum