for L being non empty transitive antisymmetric complete RelStr
for S being non empty infs-closed Subset of L
for X being Subset of S holds "/\" (X,(subrelstr S)) = "/\" (X,L)