let x be object ; :: thesis: for D being non empty set
for T being finite binary DecoratedTree of D st T = root-tree x holds
Leaves T = {x}
let D be non empty set ; :: thesis: for T being finite binary DecoratedTree of D st T = root-tree x holds
Leaves T = {x}
let T be finite binary DecoratedTree of D; :: thesis: ( T = root-tree x implies Leaves T = {x} )
assume A1: T = root-tree x ; :: thesis: Leaves T = {x}
A2: {} in elementary_tree 0 by TARSKI:def 1, TREES_1:29;
then A3: T . {} = x by A1, FUNCOP_1:7;
A4: dom T = elementary_tree 0 by FUNCT_2:def 1, A1;
A5: Leaves (dom T) = {{}} by TREES_1:29, Th15, FUNCT_2:def 1, A1;
thus Leaves T = Im (T,{}) by RELAT_1:def 16, A5
.= {x} by A3, A4, A2, FUNCT_1:59 ; :: thesis: verum