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:27, TREES_2:def 12;
set x = the Element of succ v;
the Element of succ v in succ v by A1;
then the Element of succ v in { (v ^ <*n*>) where n is Nat : v ^ <*n*> in dom p } by TREES_2:def 5;
then consider n being Nat such that
the Element of succ v = v ^ <*n*> and
A2: v ^ <*n*> in dom p ;
thus v ^ <*0*> in dom p by A2, TREES_1:def 3; :: thesis: verum