A1: {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;

let T be Tree; :: thesis: ( T = {0 ,1} * implies Leaves T = {} )
assume A2: T = {0 ,1} * ; :: thesis: Leaves T = {}
assume Leaves T <> {} ; :: thesis: contradiction
then consider x being set 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:31;
hence contradiction by A3, A5, TREES_1:def 8; :: thesis: verum