A1: RED i,j in omega ;

now

assume j <> {} ; :: thesis: ( RED j,i <> 1 implies [(RED i,j),(RED j,i)] in RAT+ )
then ( RED i,j, RED j,i are_relative_prime & RED j,i <> {} ) by Th23, Th24;
hence ( RED j,i <> 1 implies [(RED i,j),(RED j,i)] in RAT+ ) by Th39; :: thesis: verum

end;

hence ( ( j = {} implies {} is Element of RAT+ ) & ( RED j,i = 1 implies RED i,j is Element of RAT+ ) & ( not j = {} & not RED j,i = 1 implies [(RED i,j),(RED j,i)] is Element of RAT+ ) ) by A1, Lm1, Lm5; :: thesis: verum