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 = {} by TARSKI:def 1;
hence ProperPrefixes p c= {{}} by Th39, XBOOLE_1:2; :: 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