let x, y be object ; :: 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 object 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 )
A2: x in {x,y} by TARSKI:def 2;
y in {x,y} by TARSKI:def 2;
hence ( x is finite Tree & y is finite Tree ) by A1, A2; :: thesis: verum

end;

assume that
A3: x is finite Tree and
A4: y is finite Tree ; :: thesis: {x,y} is constituted-FinTrees
let z be object ; :: 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 A3, A4, TARSKI:def 2; :: thesis: verum