A b s t r a c t. A syntactic derivation of Cornish identity (J) from the axioms of HBCK is presented which amounts to a syntactic proof of Wronski's conjecture that naturally ordered BCK-algebras form a variety.