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

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

let x be object ; :: thesis: ( x in Subtrees (X1 \/ X2) implies x in (Subtrees X1) \/ (Subtrees X2) )
assume x in Subtrees (X1 \/ X2) ; :: thesis: x in (Subtrees X1) \/ (Subtrees X2)
then consider t being Element of X1 \/ X2, n being Node of t such that
A1: x = t | n by TREES_9:19;
( t in X1 or t in X2 ) by XBOOLE_0:def 3;
then ( x in Subtrees X1 or x in Subtrees X2 ) by A1, TREES_9:19;
hence x in (Subtrees X1) \/ (Subtrees X2) by XBOOLE_0:def 3; :: thesis: verum

end;

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

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

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

then consider t being Element of X1, n being Node of t such that
A3: x = t | n by TREES_9:19;
t is Element of X1 \/ X2 by XBOOLE_0:def 3;
hence x in Subtrees (X1 \/ X2) by A3, TREES_9:19; :: thesis: verum

end;

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

then consider t being Element of X2, n being Node of t such that
A4: x = t | n by TREES_9:19;
t is Element of X1 \/ X2 by XBOOLE_0:def 3;
hence x in Subtrees (X1 \/ X2) by A4, TREES_9:19; :: thesis: verum

end;

end;