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 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; :: thesis: ( ( 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] ; :: thesis: S1[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 <> {}
per cases ( k = 0 or k = 1 or k > 1 ) by NAT_1:25;
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;
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;
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 ) ) )
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
proof
per cases ( s = the Element of H or s = the Element of A or ( s <> the Element of H & s <> the Element of A ) ) ;
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;
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;
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;
end;
end;
end;
hence meet H <> {} by Th53; :: thesis: verum
end;
end;
end;
A26: for n being Nat holds S1[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