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*>)}

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;

end;

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*>)} )

hence succ t = {(t ^ <*0*>),(t ^ <*1*>)} by A3, TARSKI:2; :: thesis: verum

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

proof

succ t = { (t ^ <*n*>) where n is Nat : t ^ <*n*> in elementary_tree 2 }
by TREES_2:def 5;
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*>)} )

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;hereby :: thesis: ( x in {(t ^ <*0*>),(t ^ <*1*>)} implies x in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in elementary_tree 2 } )

assume A5:
x in {(t ^ <*0*>),(t ^ <*1*>)}
; :: thesis: 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 ;

end;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;

end;

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

hence succ t = {(t ^ <*0*>),(t ^ <*1*>)} by A3, TARSKI:2; :: thesis: verum

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

end;

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

hence
succ t = {(t ^ <*0*>),(t ^ <*1*>)}
by A1, TREES_1:54; :: thesis: verumassume A8:
t ^ <*0*> in elementary_tree 2
; :: thesis: contradiction

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

end;

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

hence
succ t = {(t ^ <*0*>),(t ^ <*1*>)}
by A1, TREES_1:54; :: thesis: verumassume A10:
t ^ <*0*> in elementary_tree 2
; :: thesis: contradiction

end;