:: deftheorem defines idempotent ROUGHS_4:def 7 :
for X being set
for f being Function of (bool X),(bool X) holds
( f is idempotent iff for A being Subset of X holds f . (f . A) = f . A );