for D being non empty set holds FinTrees D c= Trees D by Def7;