DC p is square by defDCps;
hence not X^2- (DC p) is irreducible ; :: thesis: verum