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