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

proof

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

end;

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