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