let T be Tree; :: thesis: ( T = {0 ,1} * implies Leaves T = {} )
assume A1: T = {0 ,1} * ; :: thesis: Leaves T = {}
assume Leaves T <> {} ; :: thesis: contradiction
then consider x being set such that
A2: x in Leaves T by XBOOLE_0:def 1;
reconsider x1 = x as Element of T by A2;
T is binary by A1, Th3;
then A3: x1 is FinSequence of BOOLEAN by Th2;
then reconsider x1 = x as FinSequence of NAT ;
set y1 = x1 ^ <*0 *>;
A4: 0 in {0 } by TARSKI:def 1;
{0 } c= BOOLEAN

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in {0 } or z in BOOLEAN )
assume z in {0 } ; :: thesis: z in BOOLEAN
then z = FALSE by TARSKI:def 1;
hence z in BOOLEAN ; :: thesis: verum

end;

then <*0 *> is FinSequence of BOOLEAN by A4, Lm2;
then x1 ^ <*0 *> is FinSequence of BOOLEAN by A3, Lm1;
then A5: x1 ^ <*0 *> in T by A1, FINSEQ_1:def 11;
x1 is_a_proper_prefix_of x1 ^ <*0 *> by TREES_1:31;
hence contradiction by A2, A5, TREES_1:def 8; :: thesis: verum