Description: The closure law for binary operations, see definitions of laws A0. and
M0. in section 1.1 of Hall p. 1, or definition 1 in BourbakiAlg1
p. 1: the value of a binary operation applied to two operands of a given
sets is an element of this set. By this definition, the closure law is
expressed as binary relation: a binary operation is related to a set by
clLaw if the closure law holds for this binary operation regarding
this set. Note that the binary operation needs not to be a function.
(Contributed by AV, 7-Jan-2020)