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 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;

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 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;

now :: thesis: for s being set st s in S holds

MiddleVertex (a,b,c) in s

hence
meet S <> {}
by SETFAM_1:def 1; :: thesis: verumMiddleVertex (a,b,c) in s

let s be set ; :: thesis: ( s in S implies MiddleVertex (a,b,c) in b_{1} )

assume A7: s in S ; :: thesis: MiddleVertex (a,b,c) in b_{1}

then A8: ex t being _Subtree of T st s = the_Vertices_of t by A1;

end;assume A7: s in S ; :: thesis: MiddleVertex (a,b,c) in b

then A8: ex t being _Subtree of T st 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, A7;

end;

suppose
( a in s & b in s )
; :: thesis: MiddleVertex (a,b,c) in b_{1}

then
(T .pathBetween (a,b)) .vertices() c= s
by A8, Th34;

hence MiddleVertex (a,b,c) in s by A6; :: thesis: verum

end;hence MiddleVertex (a,b,c) in s by A6; :: thesis: verum

suppose
( a in s & c in s )
; :: thesis: MiddleVertex (a,b,c) in b_{1}

then
(T .pathBetween (a,c)) .vertices() c= s
by A8, Th34;

hence MiddleVertex (a,b,c) in s by A5; :: thesis: verum

end;hence MiddleVertex (a,b,c) in s by A5; :: thesis: verum

suppose
( b in s & c in s )
; :: thesis: MiddleVertex (a,b,c) in b_{1}

then
(T .pathBetween (b,c)) .vertices() c= s
by A8, Th34;

hence MiddleVertex (a,b,c) in s by A4; :: thesis: verum

end;hence MiddleVertex (a,b,c) in s by A4; :: thesis: verum