set X = { T where T is Element of Trees : T is finite Tree } ;
{ T where T is Element of Trees : T is finite Tree } c= Trees

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { T where T is Element of Trees : T is finite Tree } or x in Trees )
assume x in { T where T is Element of Trees : T is finite Tree } ; :: thesis: x in Trees
then ex T being Element of Trees st
( x = T & T is finite Tree ) ;
hence x in Trees ; :: thesis: verum

end;

then reconsider X = { T where T is Element of Trees : T is finite Tree } as Subset of Trees ;
take X ; :: thesis: for x being set holds
( x in X iff x is finite Tree )
let x be set ; :: thesis: ( x in X iff x is finite Tree )
thus ( x in X implies x is finite Tree ) :: thesis: ( x is finite Tree implies x in X )

proof

assume x in X ; :: thesis: x is finite Tree
then ex T being Element of Trees st
( x = T & T is finite Tree ) ;
hence x is finite Tree ; :: thesis: verum

end;

assume x is finite Tree ; :: thesis: x in X
then reconsider T = x as finite Tree ;
T in Trees by Def1;
hence x in X ; :: thesis: verum