theorem Th18: :: WAYBEL23:18

for L being antisymmetric with_suprema 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 holds
sup {x,y} in S )