theorem Th4: :: REALSET1:6

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