reconsider dt = e as finite DecoratedTree ;
reconsider domdt = dom dt as finite Tree ;
take height domdt ; :: thesis: ex dt being finite DecoratedTree ex t being finite Tree st
( dt = e & t = dom dt & height domdt = height t )
take dt ; :: thesis: ex t being finite Tree st
( dt = e & t = dom dt & height domdt = height t )
take domdt ; :: thesis: ( dt = e & domdt = dom dt & height domdt = height domdt )
thus ( dt = e & domdt = dom dt & height domdt = height domdt ) ; :: thesis: verum