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

proof

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 by XBOOLE_0:def 4;
hence x is finite Tree by A1; :: thesis: verum

end;

hence Y /\ X is constituted-FinTrees ; :: 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
hence x is finite Tree by A1; :: thesis: verum