theorem Th5: :: REALSET1:7
for A being non trivial set
for x being Element of A
for F being b1 \ {b2} -subsetpreserving BinOp of A holds F || (A \ {x}) is BinOp of (A \ {x})