let p be Prime; :: thesis: 1 = 1. (GF p)
1 < p by INT_2:def 4;
then 1 in Segm p by NAT_1:44;
hence 1 = 1. (GF p) by SUBSET_1:def 8; :: thesis: verum