for p being Prime holds 0 = 0. (GF p) by NAT_1:44, SUBSET_1:def 8;