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