set L = { x where x is Element of bool (BinFinTrees D) : ( x is finite & x <> {} ) } ;

A1: now :: thesis: for z being object st z in { x where x is Element of bool (BinFinTrees D) : ( x is finite & x <> {} ) } holds
z in bool (BinFinTrees D)

let z be object ; :: thesis: ( z in { x where x is Element of bool (BinFinTrees D) : ( x is finite & x <> {} ) } implies z in bool (BinFinTrees D) )
assume z in { x where x is Element of bool (BinFinTrees D) : ( x is finite & x <> {} ) } ; :: thesis: z in bool (BinFinTrees D)
then ex x being Element of bool (BinFinTrees D) st
( x = z & x is finite & x <> {} ) ;
hence z in bool (BinFinTrees D) ; :: thesis: verum

end;

consider z being object such that
A2: z in D by XBOOLE_0:def 1;
reconsider z = z as Element of D by A2;
set T = the finite binary DecoratedTree of D;
( dom the finite binary DecoratedTree of D is finite & dom the finite binary DecoratedTree of D is binary ) by BINTREE1:def 3;
then the finite binary DecoratedTree of D in BinFinTrees D by Def2;
then reconsider x = { the finite binary DecoratedTree of D} as Element of bool (BinFinTrees D) by ZFMISC_1:31;
x in { x where x is Element of bool (BinFinTrees D) : ( x is finite & x <> {} ) } ;
hence { x where x is Element of bool (BinFinTrees D) : ( x is finite & x <> {} ) } is non empty Subset of (bool (BinFinTrees D)) by A1, TARSKI:def 3; :: thesis: verum