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