theorem Th14: :: WAYBEL14:14

for R being non empty with_suprema Poset
for l being Element of R holds
( l is co-prime iff for x, y being Element of R holds
( not l <= x "\/" y or l <= x or l <= y ) )