consider t being finite binary DecoratedTree of {{} };
take t ; :: thesis: ( t is binary & t is finite )
thus ( t is binary & t is finite ) ; :: thesis: verum