theorem Th2: :: REALSET1:2

for X being set
for F being BinOp of X
for A being Preserv of F holds F || A is BinOp of A