let n be Nat; :: thesis: n \/ {n} = n + 1
n + 1 = succ n by NAT_1:39;
hence n \/ {n} = n + 1 ; :: thesis: verum