let T be _Tree; :: thesis: for a, b, c being Vertex of T
for S being non empty set st ( for s being set st s in S 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 ) ) ) ) holds
meet S <> {}
let a, b, c be Vertex of T; :: thesis: for S being non empty set st ( for s being set st s in S 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 ) ) ) ) holds
meet S <> {}
let S be non empty set ; :: thesis: ( ( for s being set st s in S 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 ) ) ) ) implies meet S <> {} )
assume A1: for s being set st s in S 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 ) ) ) ; :: thesis: meet S <> {}
set Pab = T .pathBetween a,b;
set Pac = T .pathBetween a,c;
set Pbc = T .pathBetween b,c;
set Pca = T .pathBetween c,a;
set VPab = (T .pathBetween a,b) .vertices() ;
set VPac = (T .pathBetween a,c) .vertices() ;
set VPbc = (T .pathBetween b,c) .vertices() ;
set VPca = (T .pathBetween c,a) .vertices() ;
A2: (T .pathBetween c,a) .vertices() = (T .pathBetween a,c) .vertices() by Th31;
set m = MiddleVertex a,b,c;
(((T .pathBetween a,b) .vertices() ) /\ ((T .pathBetween b,c) .vertices() )) /\ ((T .pathBetween c,a) .vertices() ) = {(MiddleVertex a,b,c)} by Def3;
then A3: MiddleVertex a,b,c in (((T .pathBetween a,b) .vertices() ) /\ ((T .pathBetween b,c) .vertices() )) /\ ((T .pathBetween c,a) .vertices() ) by TARSKI:def 1;
then A4: MiddleVertex a,b,c in ((T .pathBetween a,b) .vertices() ) /\ ((T .pathBetween b,c) .vertices() ) by XBOOLE_0:def 4;
then A5: MiddleVertex a,b,c in (T .pathBetween a,b) .vertices() by XBOOLE_0:def 4;
A6: MiddleVertex a,b,c in (T .pathBetween a,c) .vertices() by A2, A3, XBOOLE_0:def 4;
A7: MiddleVertex a,b,c in (T .pathBetween b,c) .vertices() by A4, XBOOLE_0:def 4;

now

let s be set ; :: thesis: ( s in S implies MiddleVertex a,b,c in b₁ )
assume A8: s in S ; :: thesis: MiddleVertex a,b,c in b₁
then consider t being _Subtree of T such that
A9: s = the_Vertices_of t by A1;

per cases ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) by A1, A8;

suppose ( a in s & b in s ) ; :: thesis: MiddleVertex a,b,c in b₁

then (T .pathBetween a,b) .vertices() c= s by A9, Th33;
hence MiddleVertex a,b,c in s by A5; :: thesis: verum

end;

suppose ( a in s & c in s ) ; :: thesis: MiddleVertex a,b,c in b₁

then (T .pathBetween a,c) .vertices() c= s by A9, Th33;
hence MiddleVertex a,b,c in s by A6; :: thesis: verum

end;

suppose ( b in s & c in s ) ; :: thesis: MiddleVertex a,b,c in b₁

then (T .pathBetween b,c) .vertices() c= s by A9, Th33;
hence MiddleVertex a,b,c in s by A7; :: thesis: verum

end;

end;

end;

hence meet S <> {} by SETFAM_1:def 1; :: thesis: verum