set T = elementary_tree 2;
let t be Element of elementary_tree 2; :: according to BINTREE1:def 2 :: thesis: ( not t in Leaves (elementary_tree 2) implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} )
assume A1: not t in Leaves (elementary_tree 2) ; :: thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)}

per cases ( t = {} or t = <*0*> or t = <*1*> ) by ENUMSET1:def 1, TREES_1:53;

suppose A2: t = {} ; :: thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)}

A3: for x being object holds
( x in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in elementary_tree 2 } iff x in {(t ^ <*0*>),(t ^ <*1*>)} )

proof

let x be object ; :: thesis: ( x in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in elementary_tree 2 } iff x in {(t ^ <*0*>),(t ^ <*1*>)} )

hereby :: thesis: ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in elementary_tree 2 } )

assume x in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in elementary_tree 2 } ; :: thesis: x in {(t ^ <*0*>),(t ^ <*1*>)}
then A4: ex n being Nat st
( x = t ^ <*n*> & t ^ <*n*> in elementary_tree 2 ) ;
then reconsider x9 = x as FinSequence ;

per cases ( x = {} or x = <*0*> or x = <*1*> ) by A4, ENUMSET1:def 1, TREES_1:53;

suppose x = {} ; :: thesis: x in {(t ^ <*0*>),(t ^ <*1*>)}

hence x in {(t ^ <*0*>),(t ^ <*1*>)} by A4; :: thesis: verum

end;

suppose x = <*0*> ; :: thesis: x in {(t ^ <*0*>),(t ^ <*1*>)}

then x9 = t ^ <*0*> by A2, FINSEQ_1:34;
hence x in {(t ^ <*0*>),(t ^ <*1*>)} by TARSKI:def 2; :: thesis: verum

end;

suppose x = <*1*> ; :: thesis: x in {(t ^ <*0*>),(t ^ <*1*>)}

then x9 = t ^ <*1*> by A2, FINSEQ_1:34;
hence x in {(t ^ <*0*>),(t ^ <*1*>)} by TARSKI:def 2; :: thesis: verum

end;

end;

end;

assume A5: x in {(t ^ <*0*>),(t ^ <*1*>)} ; :: thesis: x in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in elementary_tree 2 }
then reconsider x9 = x as FinSequence by TARSKI:def 2;
A6: ( x = t ^ <*0*> or x = t ^ <*1*> ) by A5, TARSKI:def 2;
then ( x9 = <*0*> or x9 = <*1*> ) by A2, FINSEQ_1:34;
then x9 in elementary_tree 2 by ENUMSET1:def 1, TREES_1:53;
hence x in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in elementary_tree 2 } by A6; :: thesis: verum

end;

succ t = { (t ^ <*n*>) where n is Nat : t ^ <*n*> in elementary_tree 2 } by TREES_2:def 5;
hence succ t = {(t ^ <*0*>),(t ^ <*1*>)} by A3, TARSKI:2; :: thesis: verum

end;

suppose A7: t = <*0*> ; :: thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)}

now :: thesis: not t ^ <*0*> in elementary_tree 2

assume A8: t ^ <*0*> in elementary_tree 2 ; :: thesis: contradiction

per cases ( t ^ <*0*> = {} or t ^ <*0*> = <*0*> or t ^ <*0*> = <*1*> ) by A8, ENUMSET1:def 1, TREES_1:53;

suppose t ^ <*0*> = {} ; :: thesis: contradiction

hence contradiction ; :: thesis: verum

end;

suppose t ^ <*0*> = <*0*> ; :: thesis: contradiction

then (len <*0*>) + (len <*0*>) = len <*0*> by A7, FINSEQ_1:22;
hence contradiction by FINSEQ_1:39; :: thesis: verum

end;

suppose t ^ <*0*> = <*1*> ; :: thesis: contradiction

then (len <*0*>) + (len <*0*>) = len <*1*> by A7, FINSEQ_1:22;
then 1 + (len <*0*>) = len <*1*> by FINSEQ_1:39;
then 1 + 1 = len <*1*> by FINSEQ_1:39;
hence contradiction by FINSEQ_1:39; :: thesis: verum

end;

end;

end;

hence succ t = {(t ^ <*0*>),(t ^ <*1*>)} by A1, TREES_1:54; :: thesis: verum

end;

suppose A9: t = <*1*> ; :: thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)}

now :: thesis: not t ^ <*0*> in elementary_tree 2

assume A10: t ^ <*0*> in elementary_tree 2 ; :: thesis: contradiction

per cases ( t ^ <*0*> = {} or t ^ <*0*> = <*0*> or t ^ <*0*> = <*1*> ) by A10, ENUMSET1:def 1, TREES_1:53;

suppose t ^ <*0*> = {} ; :: thesis: contradiction

hence contradiction ; :: thesis: verum

end;

suppose t ^ <*0*> = <*0*> ; :: thesis: contradiction

then (len <*1*>) + (len <*0*>) = len <*0*> by A9, FINSEQ_1:22;
hence contradiction by FINSEQ_1:39; :: thesis: verum

end;

suppose t ^ <*0*> = <*1*> ; :: thesis: contradiction

then (len <*1*>) + (len <*0*>) = len <*1*> by A9, FINSEQ_1:22;
hence contradiction by FINSEQ_1:39; :: thesis: verum

end;

end;

end;

hence succ t = {(t ^ <*0*>),(t ^ <*1*>)} by A1, TREES_1:54; :: thesis: verum

end;

end;