:: deftheorem Def2 defines full BINTREE2:def 2 :
for T being Tree holds
( T is full iff T = {0,1} * );