theorem
proved
PRCPrimeCalibrationForcesTwoPrimeBranchControlsPrimesTarget_of_prime_identity_iff_two
show as:
PRCPrimeCalibrationForcesTwoPrimeBranchControlsPrimesTarget_of_prime_identity_iff_two