theorem Th16: :: WAYBEL23:16

for L being non empty RelStr
for S being Subset of L holds
( S is join-closed iff for x, y being Element of L st x in S & y in S & ex_sup_of {x,y},L holds
sup {x,y} in S )