Q0_Soundness.ZFC_in_HOL_Set_Theory