A1: now :: thesis: ( j <> {} & RED (j,i) <> 1 implies [(RED (i,j)),(RED (j,i))] in RAT+ )

assume j <> {} ; :: thesis: ( RED (j,i) <> 1 implies [(RED (i,j)),(RED (j,i))] in RAT+ )
then ( RED (i,j), RED (j,i) are_coprime & RED (j,i) <> {} ) by Th18, Th19;
hence ( RED (j,i) <> 1 implies [(RED (i,j)),(RED (j,i))] in RAT+ ) by Th33; :: thesis: verum

end;

thus ( ( 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, Lm6; :: thesis: verum