let T be Tree; :: thesis: ( T is full implies T is binary )
assume T is full ; :: thesis: T is binary
then T = {0 ,1} * by Def2;
hence T is binary by Th3; :: thesis: verum