:: deftheorem defines ||| REALSET1:def 5 :
for X being set
for A being Subset of X
for F being b₂ -subsetpreserving BinOp of X holds F ||| A = F || A;