defpred S₁[ object ] means ex T being DecoratedTree of D st
( $1 = T & dom T is finite );
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 DecoratedTree of D;
A2: dom the finite DecoratedTree of D is finite ;
the finite DecoratedTree of D in Trees D by Def7;
then A3: not X is empty by A1, A2;

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 A3, Def6;
take X ; :: thesis: for T being DecoratedTree of D holds
( dom T is finite iff T in X )
let T be DecoratedTree of D; :: thesis: ( dom T is finite iff T in X )
T in Trees D by Def7;
hence ( dom T is finite implies T in X ) by A1; :: thesis: ( T in X implies dom T is finite )
assume T in X ; :: thesis: dom T is finite
then ex t being DecoratedTree of D st
( T = t & dom t is finite ) by A1;
hence dom T is finite ; :: thesis: verum