reconsider T = {0,1} * as Tree by Th9;
take T ; :: thesis: T is full
thus T is full by Def2; :: thesis: verum