let p be Safe Prime; :: thesis: p mod 2 = 1
p >= 4 + 1 by Th2;
then p > 4 by NAT_1:13;
then p > 4 - 2 by XREAL_1:51;
then p is odd by PEPIN:17;
hence p mod 2 = 1 by NAT_2:22; :: thesis: verum