:: deftheorem Def1 defines Preserv REALSET1:def 1 :
for X being set
for F being BinOp of X
for b₃ being Subset of X holds
( b₃ is Preserv of F iff for x being set st x in [:b₃,b₃:] holds
F . x in b₃ );