theorem :: MMLQUERY:60

for X being set
for A being FinSequence of bool X
for n1, n2, m1, m2 being Nat st n1 <= m1 & n2 <= m2 holds
ROUGH (A,m1,n2) c= ROUGH (A,n1,m2)