let T be _Tree; 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; 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 ; ( ( 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 ) ) )
; meet S <> {}
set m = MiddleVertex (a,b,c);
set Pca = T .pathBetween (c,a);
set Pbc = T .pathBetween (b,c);
set Pac = T .pathBetween (a,c);
set Pab = T .pathBetween (a,b);
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() ;
(((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {(MiddleVertex (a,b,c))}
by Def3;
then A2:
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 A3:
MiddleVertex (a,b,c) in ((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())
by XBOOLE_0:def 4;
then A4:
MiddleVertex (a,b,c) in (T .pathBetween (b,c)) .vertices()
by XBOOLE_0:def 4;
(T .pathBetween (c,a)) .vertices() = (T .pathBetween (a,c)) .vertices()
by Th32;
then A5:
MiddleVertex (a,b,c) in (T .pathBetween (a,c)) .vertices()
by A2, XBOOLE_0:def 4;
A6:
MiddleVertex (a,b,c) in (T .pathBetween (a,b)) .vertices()
by A3, XBOOLE_0:def 4;
hence
meet S <> {}
by SETFAM_1:def 1; verum