let x, y be set ; :: thesis: ( {x,y} is constituted-FinTrees iff ( x is finite Tree & y is finite Tree ) )
thus ( {x,y} is constituted-FinTrees implies ( x is finite Tree & y is finite Tree ) ) :: thesis: ( x is finite Tree & y is finite Tree implies {x,y} is constituted-FinTrees )

proof

assume A1: for z being set st z in {x,y} holds
z is finite Tree ; :: according to TREES_3:def 4 :: thesis: ( x is finite Tree & y is finite Tree )
( x in {x,y} & y in {x,y} ) by TARSKI:def 2;
hence ( x is finite Tree & y is finite Tree ) by A1; :: thesis: verum

end;

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