thus z `2 is Element of (GF p) ; :: thesis: verum