:: deftheorem defines FinSeqLevel BINTREE2:def 3 :
for T being full Tree
for n being non zero Nat holds FinSeqLevel (n,T) = (NumberOnLevel (n,T)) " ;