let X, Y be set ; :: thesis: ( ( X is constituted-FinTrees & Y is constituted-FinTrees ) iff X \/ Y is constituted-FinTrees )
thus ( X is constituted-FinTrees & Y is constituted-FinTrees implies X \/ Y is constituted-FinTrees ) :: thesis: ( X \/ Y is constituted-FinTrees implies ( X is constituted-FinTrees & Y is constituted-FinTrees ) )

proof

assume that
A1: for x being object st x in X holds
x is finite Tree and
A2: for x being object st x in Y holds
x is finite Tree ; :: according to TREES_3:def 4 :: thesis: X \/ Y is constituted-FinTrees
let x be object ; :: according to TREES_3:def 4 :: thesis: ( x in X \/ Y implies x is finite Tree )
assume x in X \/ Y ; :: thesis: x is finite Tree
then ( x in X or x in Y ) by XBOOLE_0:def 3;
hence x is finite Tree by A1, A2; :: thesis: verum

end;

assume A3: for x being object st x in X \/ Y holds
x is finite Tree ; :: according to TREES_3:def 4 :: thesis: ( X is constituted-FinTrees & Y is constituted-FinTrees )
thus X is constituted-FinTrees :: thesis: Y is constituted-FinTrees

proof

let x be object ; :: according to TREES_3:def 4 :: thesis: ( x in X implies x is finite Tree )
assume x in X ; :: thesis: x is finite Tree
then x in X \/ Y by XBOOLE_0:def 3;
hence x is finite Tree by A3; :: thesis: verum

end;

let x be object ; :: according to TREES_3:def 4 :: thesis: ( x in Y implies x is finite Tree )
assume x in Y ; :: thesis: x is finite Tree
then x in X \/ Y by XBOOLE_0:def 3;
hence x is finite Tree by A3; :: thesis: verum