A1:
{0} c= BOOLEAN

assume A2: T = {0,1} * ; :: thesis: Leaves T = {}

assume Leaves T <> {} ; :: thesis: contradiction

then consider x being object such that

A3: x in Leaves T by XBOOLE_0:def 1;

reconsider x1 = x as Element of T by A3;

T is binary by A2, Th3;

then A4: x1 is FinSequence of BOOLEAN by Th2;

then reconsider x1 = x as FinSequence of NAT ;

set y1 = x1 ^ <*0*>;

0 in {0} by TARSKI:def 1;

then <*0*> is FinSequence of BOOLEAN by A1, Lm2;

then x1 ^ <*0*> is FinSequence of BOOLEAN by A4, Lm1;

then A5: x1 ^ <*0*> in T by A2, FINSEQ_1:def 11;

x1 is_a_proper_prefix_of x1 ^ <*0*> by TREES_1:8;

hence contradiction by A3, A5, TREES_1:def 5; :: thesis: verum

proof

let T be Tree; :: thesis: ( T = {0,1} * implies Leaves T = {} )
let z be object ; :: 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;assume z in {0} ; :: thesis: z in BOOLEAN

then z = FALSE by TARSKI:def 1;

hence z in BOOLEAN ; :: thesis: verum

assume A2: T = {0,1} * ; :: thesis: Leaves T = {}

assume Leaves T <> {} ; :: thesis: contradiction

then consider x being object such that

A3: x in Leaves T by XBOOLE_0:def 1;

reconsider x1 = x as Element of T by A3;

T is binary by A2, Th3;

then A4: x1 is FinSequence of BOOLEAN by Th2;

then reconsider x1 = x as FinSequence of NAT ;

set y1 = x1 ^ <*0*>;

0 in {0} by TARSKI:def 1;

then <*0*> is FinSequence of BOOLEAN by A1, Lm2;

then x1 ^ <*0*> is FinSequence of BOOLEAN by A4, Lm1;

then A5: x1 ^ <*0*> in T by A2, FINSEQ_1:def 11;

x1 is_a_proper_prefix_of x1 ^ <*0*> by TREES_1:8;

hence contradiction by A3, A5, TREES_1:def 5; :: thesis: verum