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

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