set T = elementary_tree 2;
let t be Element of elementary_tree 2; :: according to BINTREE1:def 2 :: thesis: ( not t in Leaves () implies succ t = {(),(t ^ <*1*>)} )
assume A1: not t in Leaves () ; :: thesis: succ t = {(),(t ^ <*1*>)}
per cases ( t = {} or t = or t = <*1*> ) by ;
suppose A2: t = {} ; :: thesis: succ t = {(),(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 ^ <*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 ^ <*1*>)} )
hereby :: thesis: ( x in {(),(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 ^ <*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 = or x = <*1*> ) by ;
suppose x = {} ; :: thesis: x in {(),(t ^ <*1*>)}
hence x in {(),(t ^ <*1*>)} by A4; :: thesis: verum
end;
suppose x = ; :: thesis: x in {(),(t ^ <*1*>)}
then x9 = t ^ by ;
hence x in {(),(t ^ <*1*>)} by TARSKI:def 2; :: thesis: verum
end;
end;
end;
assume A5: x in {(),(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 ^ or x = t ^ <*1*> ) by ;
then ( x9 = or x9 = <*1*> ) by ;
then x9 in elementary_tree 2 by ;
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 ^ <*1*>)} by ; :: thesis: verum
end;
suppose A7: t = ; :: thesis: succ t = {(),(t ^ <*1*>)}
now :: thesis:
assume A8: t ^ in elementary_tree 2 ; :: thesis: contradiction
per cases by ;
suppose t ^ = ; :: thesis: contradiction
end;
suppose t ^ = <*1*> ; :: thesis: contradiction
end;
end;
end;
hence succ t = {(),(t ^ <*1*>)} by ; :: thesis: verum
end;
suppose A9: t = <*1*> ; :: thesis: succ t = {(),(t ^ <*1*>)}
end;
end;