let a, b be non zero Integer; :: thesis: ( min ((Parity a),(Parity b)) divides a & min ((Parity a),(Parity b)) divides b )
( min ((Parity a),(Parity b)) = Parity a or min ((Parity a),(Parity b)) = Parity b ) by XXREAL_0:def 9;
then A1: ( min ((Parity a),(Parity b)) divides Parity a & min ((Parity a),(Parity b)) divides Parity b ) by XXREAL_0:def 9, PEPIN31;
( Parity a divides a & Parity b divides b ) by Th3;
hence ( min ((Parity a),(Parity b)) divides a & min ((Parity a),(Parity b)) divides b ) by A1, INT_2:9; :: thesis: verum