set X = { T where T is Subset of (NAT *) : T is Tree } ;
take { T where T is Subset of (NAT *) : T is Tree } ; :: thesis: for x being object holds
( x in { T where T is Subset of (NAT *) : T is Tree } iff x is Tree )
let x be object ; :: thesis: ( x in { T where T is Subset of (NAT *) : T is Tree } iff x is Tree )
thus ( x in { T where T is Subset of (NAT *) : T is Tree } implies x is Tree ) :: thesis: ( x is Tree implies x in { T where T is Subset of (NAT *) : T is Tree } )

proof

assume x in { T where T is Subset of (NAT *) : T is Tree } ; :: thesis: x is Tree
then ex T being Subset of (NAT *) st
( x = T & T is Tree ) ;
hence x is Tree ; :: thesis: verum

end;

assume x is Tree ; :: thesis: x in { T where T is Subset of (NAT *) : T is Tree }
then reconsider T = x as Tree ;
T is Subset of (NAT *) by TREES_1:def 3;
hence x in { T where T is Subset of (NAT *) : T is Tree } ; :: thesis: verum