A1:
now assume
j <> {}
;
( 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;
verum end;
RED (i,j) in omega
;
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; verum