let x be object ; :: thesis: root-tree x = {[{},x]}
thus root-tree x = [:{{}},{x}:] by FUNCOP_1:def 2, TREES_1:29
.= {[{},x]} by ZFMISC_1:29 ; :: thesis: verum