theorem Th24: :: WAYBEL12:24

for L being transitive antisymmetric with_infima RelStr
for V being Subset of L holds { x where x is Element of L : V "/\" {x} c= V } is filtered Subset of L