1.  k = sk        (ipotesi)
2.  kP = kP       (assioma refl.)
3.  kP = skP      (cong2)(1.2.)
4.  kPQ = kPQ     (assioma refl)
5.  kPQ = skPQ    (congr)(3.4.)
6.  kPQ = P       (Axk)
7.  skPQ = kPQ    (symm.)(5.) 
8.  skPQ = P      (trans)(7.6.)
9.  skPQ = kQ(PQ) (Axs)
10. kQ(PQ) = Q    (Axk)
11. skPQ = Q      (trans)(9.10.)
12. P = skPQ      (symm.)(8.)
13. P = Q         (trans)(12.11.)

La dimostrazione fornita e' indipendente da cosa siano realmente i due termini
P e Q. Sostituendo a P e Q due qualsiasi termini specifici, si ottiene
quindi una prova della loro uguaglianza.
Abbiamo cosi' dimostrato che ogni possibile fbf di CL e' derivabile
dall'ipotesi k=ks.
L'insieme {k=ks} e' quindi inconsistente.