:: deftheorem Def4 defines Presv REALSET1:def 4 :
for X being set
for A being Subset of X
for b₃ being BinOp of X holds
( b₃ is Presv of X,A iff for x being set st x in [:A,A:] holds
b₃ . x in A );