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

proof

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

end;

hence Y /\ X is constituted-Trees ; :: thesis: X \ Y is constituted-Trees
let x be object ; :: according to TREES_3:def 3 :: thesis: ( x in X \ Y implies x is Tree )
assume x in X \ Y ; :: thesis: x is Tree
hence x is Tree by A1; :: thesis: verum