let X1, X2 be non empty constituted-DTrees set ; :: thesis: for C being set holds C -Subtrees (X1 \/ X2) = (C -Subtrees X1) \/ (C -Subtrees X2)
let C be set ; :: thesis: C -Subtrees (X1 \/ X2) = (C -Subtrees X1) \/ (C -Subtrees X2)

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: (C -Subtrees X1) \/ (C -Subtrees X2) c= C -Subtrees (X1 \/ X2)

let x be object ; :: thesis: ( x in C -Subtrees (X1 \/ X2) implies x in (C -Subtrees X1) \/ (C -Subtrees X2) )
assume x in C -Subtrees (X1 \/ X2) ; :: thesis: x in (C -Subtrees X1) \/ (C -Subtrees X2)
then consider t being Element of X1 \/ X2, n being Node of t such that
A1: x = t | n and
A2: ( not n in Leaves (dom t) or t . n in C ) by TREES_9:24;
( t in X1 or t in X2 ) by XBOOLE_0:def 3;
then ( x in C -Subtrees X1 or x in C -Subtrees X2 ) by A1, A2, TREES_9:24;
hence x in (C -Subtrees X1) \/ (C -Subtrees X2) by XBOOLE_0:def 3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (C -Subtrees X1) \/ (C -Subtrees X2) or x in C -Subtrees (X1 \/ X2) )
assume A3: x in (C -Subtrees X1) \/ (C -Subtrees X2) ; :: thesis: x in C -Subtrees (X1 \/ X2)

per cases ( x in C -Subtrees X1 or x in C -Subtrees X2 ) by A3, XBOOLE_0:def 3;

suppose x in C -Subtrees X1 ; :: thesis: x in C -Subtrees (X1 \/ X2)

then consider t being Element of X1, n being Node of t such that
A4: x = t | n and
A5: ( not n in Leaves (dom t) or t . n in C ) by TREES_9:24;
t is Element of X1 \/ X2 by XBOOLE_0:def 3;
hence x in C -Subtrees (X1 \/ X2) by A4, A5, TREES_9:24; :: thesis: verum

end;

suppose x in C -Subtrees X2 ; :: thesis: x in C -Subtrees (X1 \/ X2)

then consider t being Element of X2, n being Node of t such that
A6: x = t | n and
A7: ( not n in Leaves (dom t) or t . n in C ) by TREES_9:24;
t is Element of X1 \/ X2 by XBOOLE_0:def 3;
hence x in C -Subtrees (X1 \/ X2) by A6, A7, TREES_9:24; :: thesis: verum

end;

end;