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