let s be 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 )
let p be 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 )
let v be Element of dom p; ( branchdeg v = 2 implies ( v ^ <*0*> in dom p & v ^ <*1*> in dom p ) )
A1:
succ v = { (v ^ <*n*>) where n is Nat : v ^ <*n*> in dom p }
by TREES_2:def 5;
assume
branchdeg v = 2
; ( v ^ <*0*> in dom p & v ^ <*1*> in dom p )
then
card (succ v) = 2
by TREES_2:def 12;
then consider x, y being object such that
A2:
x <> y
and
A3:
succ v = {x,y}
by CARD_2:60;
x in succ v
by A3, TARSKI:def 2;
then consider n being Nat such that
A4:
x = v ^ <*n*>
and
A5:
v ^ <*n*> in dom p
by A1;
y in succ v
by A3, TARSKI:def 2;
then consider k being Nat such that
A6:
y = v ^ <*k*>
and
A7:
v ^ <*k*> in dom p
by A1;
( n <> 0 or k <> 0 )
by A2, A4, A6;
then A8:
( n > 0 or k > 0 )
;
thus
v ^ <*0*> in dom p
by A5, TREES_1:def 3; v ^ <*1*> in dom p
( n >= 0 + 1 or k >= 0 + 1 )
by A8, NAT_1:13;
hence
v ^ <*1*> in dom p
by A5, A7, TREES_1:def 3; verum