A1: {0} c= BOOLEAN
proof
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;
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 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