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

proof

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

end;

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