theorem :: PRE_CIRC:19

for x being set holds card (root-tree x) = 1