A1:
now ( j <> {} & RED (j,i) <> 1 implies [(RED (i,j)),(RED (j,i))] in RAT+ )assume
j <> {}
;
( 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;
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; verum