for D being non empty set
for f being BinOp of D holds
( f is cancelable iff ( f is left-cancelable & f is right-cancelable ) ) ;