for L being transitive antisymmetric with_infima RelStr
for S being non empty meet-closed Subset of L holds subrelstr S is with_infima