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