theorem Th4: :: REALSET1:6
for X being set
for A being Subset of X
for F being b2 -subsetpreserving BinOp of X holds F || A is BinOp of A