theorem :: MMLQUERY:59

for X being set
for n, m being Nat
for A being FinSequence of bool X st n <= m holds
ROUGH (A,m) c= ROUGH (A,n)