PrimeDivisors 1 = {} by NUMBER12:51;
hence card (PrimeDivisors 1) = 0 ; :: thesis: verum