let n be Nat; :: thesis: n c= n + 1
n + 1 = n \/ {n} by AFINSQ_1:2;
hence n c= n + 1 by XBOOLE_1:7; :: thesis: verum