theorem :: YELLOW_4:51

for L being reflexive antisymmetric with_infima RelStr
for D being Subset of L
for x being Element of L st x is_>=_than D holds
{x} "/\" D = D