Description: Reverse closure for the first argument of a Sylow P -subgroup. (Contributed by Mario Carneiro, 16-Jan-2015) (Revised by Mario Carneiro, 2-May-2015)