let i, j be Element of omega ; :: thesis: ( [i,j] in RAT+ iff ( i,j are_relative_prime & j <> {} & j <> 1 ) )
A1: not [i,j] in omega by Th38;

hereby :: thesis: ( i,j are_relative_prime & j <> {} & j <> 1 implies [i,j] in RAT+ )

assume [i,j] in RAT+ ; :: thesis: ( i,j are_relative_prime & j <> {} & j <> 1 )
then A2: [i,j] in RATplus \ { [k,1] where k is Element of omega : verum } by A1, XBOOLE_0:def 3;
then A3: ( [i,j] in RATplus & not [i,j] in { [k,1] where k is Element of omega : verum } ) by XBOOLE_0:def 5;
thus ( i,j are_relative_prime & j <> {} ) by A2, Lm4; :: thesis: j <> 1
thus j <> 1 by A3; :: thesis: verum

end;

assume ( i,j are_relative_prime & j <> {} ) ; :: thesis: ( not j <> 1 or [i,j] in RAT+ )
then A4: [i,j] in RATplus ;
assume j <> 1 ; :: thesis: [i,j] in RAT+
then for k being Element of omega holds not [i,j] = [k,1] by ZFMISC_1:33;
then not [i,j] in { [k,1] where k is Element of omega : verum } ;
then [i,j] in RATplus \ { [k,1] where k is Element of omega : verum } by A4, XBOOLE_0:def 5;
hence [i,j] in RAT+ by XBOOLE_0:def 3; :: thesis: verum