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

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

assume [i,j] in RAT+ ; :: thesis: ( i,j are_coprime & j <> {} & j <> 1 )
then A2: [i,j] in { [a,b] where a, b is Element of omega : ( a,b are_coprime & b <> {} ) } \ { [k,1] where k is Element of omega : verum } by A1, XBOOLE_0:def 3;
hence ( i,j are_coprime & j <> {} ) by Lm5; :: thesis: j <> 1
not [i,j] in { [k,1] where k is Element of omega : verum } by A2, XBOOLE_0:def 5;
hence j <> 1 ; :: thesis: verum

end;

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