let s be non empty typealg ; :: thesis: for p being Proof of s
for v being Element of dom p st branchdeg v = 1 holds
v ^ <*0 *> in dom p
let p be Proof of s; :: thesis: for v being Element of dom p st branchdeg v = 1 holds
v ^ <*0 *> in dom p
let v be Element of dom p; :: thesis: ( branchdeg v = 1 implies v ^ <*0 *> in dom p )
assume branchdeg v = 1 ; :: thesis: v ^ <*0 *> in dom p
then A1: succ v <> {} by CARD_1:47, TREES_2:def 13;
consider x being Element of succ v;
x in succ v by A1;
then x in { (v ^ <*n*>) where n is Element of NAT : v ^ <*n*> in dom p } by TREES_2:def 5;
then consider n being Element of NAT such that
x = v ^ <*n*> and
A2: v ^ <*n*> in dom p ;
0 <= n by NAT_1:2;
hence v ^ <*0 *> in dom p by A2, TREES_1:def 5; :: thesis: verum