let X be set ; :: thesis: ( X is constituted-Trees iff X c= Trees )
thus ( X is constituted-Trees implies X c= Trees ) :: thesis: ( X c= Trees implies X is constituted-Trees )

proof

assume A1: for x being object st x in X holds
x is Tree ; :: according to TREES_3:def 3 :: thesis: X c= Trees
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Trees )
assume x in X ; :: thesis: x in Trees
then x is Tree by A1;
hence x in Trees by Def1; :: thesis: verum

end;

assume A2: X c= Trees ; :: thesis: X is constituted-Trees
let x be object ; :: according to TREES_3:def 3 :: thesis: ( x in X implies x is Tree )
assume x in X ; :: thesis: x is Tree
hence x is Tree by A2, Def1; :: thesis: verum