:: deftheorem defines ! REALSET1:def 7 :
for A being non trivial set
for x being Element of A
for F being b₁ \ {b₂} -subsetpreserving BinOp of A holds F ! (A,x) = F || (A \ {x});