defpred S₁[ object ] means ex T being DecoratedTree of D st
( $1 = T & dom T is finite & T is binary );
consider X being set such that
A1: for x being object holds
( x in X iff ( x in Trees D & S₁[x] ) ) from XBOOLE_0:sch 1();
set T = the finite binary DecoratedTree of D;
dom the finite binary DecoratedTree of D is binary by BINTREE1:def 3;
then A2: not X is empty by A1, TREES_3:def 7;

now :: thesis: for x being object st x in X holds
x is DecoratedTree of D

let x be object ; :: thesis: ( x in X implies x is DecoratedTree of D )
assume x in X ; :: thesis: x is DecoratedTree of D
then x in Trees D by A1;
hence x is DecoratedTree of D ; :: thesis: verum

end;

then reconsider X = X as DTree-set of D by A2, TREES_3:def 6;
take X ; :: thesis: for T being DecoratedTree of D holds
( ( dom T is finite & T is binary ) iff T in X )
let T be DecoratedTree of D; :: thesis: ( ( dom T is finite & T is binary ) iff T in X )
thus ( dom T is finite & T is binary implies T in X ) by A1, TREES_3:def 7; :: thesis: ( T in X implies ( dom T is finite & T is binary ) )
assume T in X ; :: thesis: ( dom T is finite & T is binary )
then ex t being DecoratedTree of D st
( T = t & dom t is finite & t is binary ) by A1;
hence ( dom T is finite & T is binary ) ; :: thesis: verum