let p, q be Prime; :: thesis: for a, b being Nat st a <> 1 & b <> 1 & p * q = a * b & not ( p = a & q = b ) holds
( p = b & q = a )
let a, b be Nat; :: thesis: ( a <> 1 & b <> 1 & p * q = a * b & not ( p = a & q = b ) implies ( p = b & q = a ) )
assume that
A1: a <> 1 and
A2: b <> 1 and
A3: p * q = a * b and
A4: ( p <> a or q <> b ) ; :: thesis: ( p = b & q = a )
a divides a * b ;

per cases then ( a = p or a = q or a = p * q ) by A1, A3, GR_CY_3:1;

suppose A5: a = p ; :: thesis: ( p = b & q = a )

then q <> b by A4;
hence ( p = b & q = a ) by A3, A5, XCMPLX_1:5; :: thesis: verum

end;

suppose a = q ; :: thesis: ( p = b & q = a )

hence ( p = b & q = a ) by A3, XCMPLX_1:5; :: thesis: verum

end;

suppose A6: a = p * q ; :: thesis: ( p = b & q = a )

then a * 1 = a * b by A3;
hence ( p = b & q = a ) by A2, A6, XCMPLX_1:5; :: thesis: verum

end;

end;