:: deftheorem defines co-prime WAYBEL_6:def 8 :
for L being non empty RelStr
for l being Element of L holds
( l is co-prime iff l ~ is prime );