let x be set ; :: thesis: card (root-tree x) = 1
root-tree x = {[{},x]} by TREES_4:6;
hence card (root-tree x) = 1 by CARD_1:30; :: thesis: verum