set D = {{} };
{{} } is Tree-like

proof

thus {{} } c= NAT * :: according to TREES_1:def 5 :: thesis: ( ( for p being FinSequence of NAT st p in {{} } holds
ProperPrefixes p c= {{} } ) & ( for p being FinSequence of NAT
for k, n being Element of NAT st p ^ <*k*> in {{} } & n <= k holds
p ^ <*n*> in {{} } ) )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {{} } or x in NAT * )
assume x in {{} } ; :: thesis: x in NAT *
then x = {} by TARSKI:def 1;
hence x in NAT * by FINSEQ_1:66; :: thesis: verum

end;

thus for p being FinSequence of NAT st p in {{} } holds
ProperPrefixes p c= {{} } :: thesis: for p being FinSequence of NAT
for k, n being Element of NAT st p ^ <*k*> in {{} } & n <= k holds
p ^ <*n*> in {{} }

proof

let p be FinSequence of NAT ; :: thesis: ( p in {{} } implies ProperPrefixes p c= {{} } )
assume p in {{} } ; :: thesis: ProperPrefixes p c= {{} }
then ( p = {} & {} c= {{} } ) by TARSKI:def 1, XBOOLE_1:2;
hence ProperPrefixes p c= {{} } by Th39; :: thesis: verum

end;

let p be FinSequence of NAT ; :: thesis: for k, n being Element of NAT st p ^ <*k*> in {{} } & n <= k holds
p ^ <*n*> in {{} }
let k, n be Element of NAT ; :: thesis: ( p ^ <*k*> in {{} } & n <= k implies p ^ <*n*> in {{} } )
assume p ^ <*k*> in {{} } ; :: thesis: ( not n <= k or p ^ <*n*> in {{} } )
hence ( not n <= k or p ^ <*n*> in {{} } ) by TARSKI:def 1; :: thesis: verum

end;

hence {{} } is Tree ; :: thesis: verum