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;
now :: thesis: for s being set st s in S holds
MiddleVertex (a,b,c) in s
let s be set ; :: thesis: ( s in S implies MiddleVertex (a,b,c) in b1 )
assume A7: s in S ; :: thesis: MiddleVertex (a,b,c) in b1
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;
suppose ( a in s & b in s ) ; :: thesis: MiddleVertex (a,b,c) in b1
then (T .pathBetween (a,b)) .vertices() c= s by A8, Th34;
hence MiddleVertex (a,b,c) in s by A6; :: thesis: verum
end;
suppose ( a in s & c in s ) ; :: thesis: MiddleVertex (a,b,c) in b1
then (T .pathBetween (a,c)) .vertices() c= s by A8, Th34;
hence MiddleVertex (a,b,c) in s by A5; :: thesis: verum
end;
suppose ( b in s & c in s ) ; :: thesis: MiddleVertex (a,b,c) in b1
then (T .pathBetween (b,c)) .vertices() c= s by A8, Th34;
hence MiddleVertex (a,b,c) in s by A4; :: thesis: verum
end;
end;
end;
hence meet S <> {} by SETFAM_1:def 1; :: thesis: verum