:: deftheorem defines Root MODAL_1:def 1 :
for Z being Tree holds Root Z = {} ;