set X = DTConUA f,D;
set A = { (root-tree d) where d is Symbol of (DTConUA f,D) : d in Terminals (DTConUA f,D) } ;
{ (root-tree d) where d is Symbol of (DTConUA f,D) : d in Terminals (DTConUA f,D) } c= the carrier of (FreeUnivAlgZAO f,D)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (root-tree d) where d is Symbol of (DTConUA f,D) : d in Terminals (DTConUA f,D) } or x in the carrier of (FreeUnivAlgZAO f,D) )
assume x in { (root-tree d) where d is Symbol of (DTConUA f,D) : d in Terminals (DTConUA f,D) } ; :: thesis: x in the carrier of (FreeUnivAlgZAO f,D)
then ex d being Symbol of (DTConUA f,D) st
( x = root-tree d & d in Terminals (DTConUA f,D) ) ;
hence x in the carrier of (FreeUnivAlgZAO f,D) by DTCONSTR:def 4; :: thesis: verum

end;

hence { (root-tree s) where s is Symbol of (DTConUA f,D) : s in Terminals (DTConUA f,D) } is Subset of (FreeUnivAlgZAO f,D) ; :: thesis: verum