let x be object ; :: thesis: ( {x} is constituted-Trees iff x is Tree )
thus ( {x} is constituted-Trees implies x is Tree ) :: thesis: ( x is Tree implies {x} is constituted-Trees )

proof

assume A1: for y being object st y in {x} holds
y is Tree ; :: according to TREES_3:def 3 :: thesis: x is Tree
x in {x} by TARSKI:def 1;
hence x is Tree by A1; :: thesis: verum

end;

assume A2: x is Tree ; :: thesis: {x} is constituted-Trees
let y be object ; :: according to TREES_3:def 3 :: thesis: ( y in {x} implies y is Tree )
thus ( y in {x} implies y is Tree ) by A2, TARSKI:def 1; :: thesis: verum