:: deftheorem defines = TREES_2:def 1 :
for W1, W2 being Tree holds
( W1 = W2 iff for p being FinSequence of NAT holds
( p in W1 iff p in W2 ) );