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₁[ 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₁[n] ) holds
S₁[k]

proof

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S₁[n] ) implies S₁[k] )
assume A3: for n being Nat st n < k holds
S₁[n] ; :: thesis: S₁[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:26;

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

hence meet H <> {} by A4; :: thesis: verum

end;

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

then consider x being Element of H such that
A7: H = {x} by A4, GRAPH_5:7;
x in H ;
then ex t being _Subtree of T st x = the_Vertices_of t by A1, A5;
hence meet H <> {} by A7, SETFAM_1:11; :: thesis: verum

end;

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

set cH = choose H;
set A = H \ {(choose H)};
A9: card (H \ {(choose H)}) = (card H) - (card {(choose H)}) by EULER_1:5
.= k - 1 by A4, CARD_1:50 ;
k - 1 > 1 - 1 by A8, XREAL_1:11;
then reconsider A = H \ {(choose H)} as non empty finite set by A9;
set cA = choose A;
A10: ( choose A in A & A c= H ) ;
set B = H \ {(choose A)};
set C = {(choose H),(choose A)};
A11: choose A <> choose H by ZFMISC_1:64;
A12: A c= X by A5, XBOOLE_1:1;
A13: for x, y being set st x in A & y in A holds
x meets y by A6;
card A < k by A9, XREAL_1:46;
then reconsider mA = meet A as non empty set by A3, A12, A13;
A14: card (H \ {(choose A)}) = (card H) - (card {(choose A)}) by A10, EULER_1:5
.= k - 1 by A4, CARD_1:50 ;
k - 1 > 1 - 1 by A8, XREAL_1:11;
then reconsider B = H \ {(choose A)} as non empty finite set by A14;
A15: B c= X by A5, XBOOLE_1:1;
A16: for x, y being set st x in B & y in B holds
x meets y by A6;
card B < k by A14, XREAL_1:46;
then reconsider mB = meet B as non empty set by A3, A15, A16;
A17: choose H meets choose A by A6, A10;
meet {(choose H),(choose A)} = (choose H) /\ (choose A) by SETFAM_1:12;
then reconsider mC = meet {(choose H),(choose A)} as non empty set by A17, XBOOLE_0:def 7;
choose H in H ;
then A18: {(choose H),(choose A)} c= X by A5, A10, A12, ZFMISC_1:38;
set a = choose mA;
set b = choose mB;
set c = choose mC;
A19: choose mA in mA ;
mA c= union A by SETFAM_1:3;
then consider aa being set such that
A20: choose mA in aa and
A21: aa in A by A19, TARSKI:def 4;
consider aat being _Subtree of T such that
A22: aa = the_Vertices_of aat by A1, A12, A21;
A23: choose mB in mB ;
mB c= union B by SETFAM_1:3;
then consider bb being set such that
A24: choose mB in bb and
A25: bb in B by A23, TARSKI:def 4;
consider bbt being _Subtree of T such that
A26: bb = the_Vertices_of bbt by A1, A15, A25;
A27: choose mC in mC ;
mC c= union {(choose H),(choose A)} by SETFAM_1:3;
then consider cc being set such that
A28: choose mC in cc and
A29: cc in {(choose H),(choose A)} by A27, TARSKI:def 4;
consider cct being _Subtree of T such that
A30: cc = the_Vertices_of cct by A1, A18, A29;
reconsider a = choose mA, b = choose mB, c = choose mC as Vertex of T by A20, A22, A24, A26, A28, A30;

now

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 A31: 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 = choose H or s = choose A or ( s <> choose H & s <> choose A ) ) ;

suppose A32: s = choose H ; :: thesis: ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) )

then A33: s in {(choose H),(choose A)} by TARSKI:def 2;
s in B by A11, A32, ZFMISC_1:64;
hence ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) by A33, SETFAM_1:def 1; :: thesis: verum

end;

suppose A34: s = choose 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 {(choose H),(choose 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 A34, SETFAM_1:def 1; :: thesis: verum

end;

suppose ( s <> choose H & s <> choose 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 A31, ZFMISC_1:64;
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 Th52; :: thesis: verum

end;

end;

end;

A35: for n being Nat holds S₁[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
A36: H c= X and
A37: for x, y being set st x in H & y in H holds
x meets y ; :: thesis: meet H <> {}
reconsider H' = H as finite set by A36;
card H' = card H' ;
hence meet H <> {} by A35, A36, A37; :: thesis: verum