let c be set ; :: thesis: Leaves (root-tree c) = {c}
thus Leaves (root-tree c) = (root-tree c) .: (Leaves (elementary_tree 0))
.= ({{}} --> c) .: (dom ({{}} --> c)) by TREES_1:29, HUFFMAN1:15
.= rng ({{}} --> c) by RELAT_1:113
.= {c} by FUNCOP_1:8 ; :: thesis: verum