theorem :: WAYBEL15:19

for L being non empty RelStr
for x being Element of L holds
( x in PRIME (L opp) iff x is co-prime )