theorem Th2: :: REALSET1:2

for X being set
for F being BinOp of X
for A being b₂ -binopclosed Subset of X holds F || A is BinOp of A