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