let x be Element of (FreeUnivAlgNSG f,D); :: thesis: x is DecoratedTree-like
x is Element of TS (DTConUA f,D) ;
hence x is DecoratedTree-like ; :: thesis: verum