theorem Th17: :: WAYBEL12:17

for L being transitive antisymmetric with_infima RelStr
for V being Subset of L
for x, y being Element of L st x <= y holds
{y} "/\" V is_coarser_than {x} "/\" V