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

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