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

proof

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

end;

assume that
A3: x is Tree and
A4: y is Tree ; :: thesis: {x,y} is constituted-Trees
let z be object ; :: according to TREES_3:def 3 :: thesis: ( z in {x,y} implies z is Tree )
thus ( z in {x,y} implies z is Tree ) by A3, A4, TARSKI:def 2; :: thesis: verum