take D = {(<*> NAT )}; :: thesis: ( not D is empty & D is Tree-like )
thus not D is empty ; :: thesis: D is Tree-like
thus D c= NAT * :: according to TREES_1:def 5 :: thesis: ( ( for p being FinSequence of NAT st p in D holds
ProperPrefixes p c= D ) & ( for p being FinSequence of NAT
for k, n being Element of NAT st p ^ <*k*> in D & n <= k holds
p ^ <*n*> in D ) )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in D or x in NAT * )
assume A1: x in D ; :: thesis: x in NAT *
A2: x = <*> NAT by A1, TARSKI:def 1;
thus x in NAT * by A2, FINSEQ_1:def 11; :: thesis: verum

end;

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

proof

let p be FinSequence of NAT ; :: thesis: ( p in D implies ProperPrefixes p c= D )
assume A3: p in D ; :: thesis: ProperPrefixes p c= D
A4: p = <*> NAT by A3, TARSKI:def 1;
thus ProperPrefixes p c= D by A4, 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 D & n <= k holds
p ^ <*n*> in D
let k, n be Element of NAT ; :: thesis: ( p ^ <*k*> in D & n <= k implies p ^ <*n*> in D )
assume A5: p ^ <*k*> in D ; :: thesis: ( not n <= k or p ^ <*n*> in D )
thus ( not n <= k or p ^ <*n*> in D ) by A5, TARSKI:def 1; :: thesis: verum