:: deftheorem defBB defines BinBranch NTALGO_2:def 1 :
for a, b being object
for c being Nat holds
( ( c = 0 implies BinBranch (a,b,c) = a ) & ( not c = 0 implies BinBranch (a,b,c) = b ) );