:: deftheorem defines join-irreducible WAYBEL_6:def 3 :
for G being non empty RelStr
for g being Element of G holds
( g is join-irreducible iff for x, y being Element of G holds
( not g = x "\/" y or x = g or y = g ) );