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

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

suppose 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 ( s in {(choose H),(choose A)} & s in B ) by A23, TARSKI:def 2, 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;

suppose A25: 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 A25, 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 A24, 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 Th53; :: thesis: verum

end;

end;

end;

A26: 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
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