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 (FreeUnivAlgNSG (f,D))
proof
let x be object ; :: 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 (FreeUnivAlgNSG (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 (FreeUnivAlgNSG (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 (FreeUnivAlgNSG (f,D)) by DTCONSTR:def 1; :: thesis: verum
end;
hence { (root-tree s) where s is Symbol of (DTConUA (f,D)) : s in Terminals (DTConUA (f,D)) } is Subset of (FreeUnivAlgNSG (f,D)) ; :: thesis: verum