for L being non empty transitive RelStr
for S being non empty meet-closed Subset of L
for x, y being Element of S st ex_inf_of {x,y},L holds
( ex_inf_of {x,y}, subrelstr S & "/\" ({x,y},(subrelstr S)) = "/\" ({x,y},L) )