set t = the finite binary DecoratedTree of {{}};
take the finite binary DecoratedTree of {{}} ; :: thesis: ( the finite binary DecoratedTree of {{}} is binary & the finite binary DecoratedTree of {{}} is finite )
thus ( the finite binary DecoratedTree of {{}} is binary & the finite binary DecoratedTree of {{}} is finite ) ; :: thesis: verum