set D = {{} };
A1: {{} } 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 A2: x in {{} } ; :: thesis: x in NAT *
A3: x = {} by A2, TARSKI:def 1;
thus x in NAT * by A3, 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 A4: p in {{} } ; :: thesis: ProperPrefixes p c= {{} }
A5: p = {} by A4, TARSKI:def 1;
thus ProperPrefixes p c= {{} } by A5, 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 A6: p ^ <*k*> in {{} } ; :: thesis: ( not n <= k or p ^ <*n*> in {{} } )
thus ( not n <= k or p ^ <*n*> in {{} } ) by A6, TARSKI:def 1; :: thesis: verum

end;

thus {{} } is Tree by A1; :: thesis: verum