theorem Th1: :: PRELAMB:1

for s being non empty typealg
for p being Proof of s
for v being Element of dom p st branchdeg v = 1 holds
v ^ <*0*> in dom p