C o n ( Z F + ¬ A C ) Con(ZF+\neg AC)