let X be set ; :: thesis: 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)

let A be FinSequence of bool X; :: thesis: for n1, n2, m1, m2 being Nat st n1 <= m1 & n2 <= m2 holds

ROUGH (A,m1,n2) c= ROUGH (A,n1,m2)

let n1, n2, m1, m2 be Nat; :: thesis: ( n1 <= m1 & n2 <= m2 implies ROUGH (A,m1,n2) c= ROUGH (A,n1,m2) )

assume A1: n1 <= m1 ; :: thesis: ( not n2 <= m2 or ROUGH (A,m1,n2) c= ROUGH (A,n1,m2) )

assume A2: n2 <= m2 ; :: thesis: ROUGH (A,m1,n2) c= ROUGH (A,n1,m2)

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in ROUGH (A,m1,n2) or z in ROUGH (A,n1,m2) )

assume A3: z in ROUGH (A,m1,n2) ; :: thesis: z in ROUGH (A,n1,m2)

then z in { x where x is Element of X : ( m1 <= #occurrences (x,A) & #occurrences (x,A) <= n2 ) } by Def25;

then consider a being Element of X such that

A4: ( z = a & m1 <= #occurrences (a,A) & #occurrences (a,A) <= n2 ) ;

( n1 <= #occurrences (a,A) & #occurrences (a,A) <= m2 ) by A1, A2, A4, XXREAL_0:2;

then z in { x where x is Element of X : ( n1 <= #occurrences (x,A) & #occurrences (x,A) <= m2 ) } by A4;

hence z in ROUGH (A,n1,m2) by A3, Def25; :: thesis: verum

for n1, n2, m1, m2 being Nat st n1 <= m1 & n2 <= m2 holds

ROUGH (A,m1,n2) c= ROUGH (A,n1,m2)

let A be FinSequence of bool X; :: thesis: for n1, n2, m1, m2 being Nat st n1 <= m1 & n2 <= m2 holds

ROUGH (A,m1,n2) c= ROUGH (A,n1,m2)

let n1, n2, m1, m2 be Nat; :: thesis: ( n1 <= m1 & n2 <= m2 implies ROUGH (A,m1,n2) c= ROUGH (A,n1,m2) )

assume A1: n1 <= m1 ; :: thesis: ( not n2 <= m2 or ROUGH (A,m1,n2) c= ROUGH (A,n1,m2) )

assume A2: n2 <= m2 ; :: thesis: ROUGH (A,m1,n2) c= ROUGH (A,n1,m2)

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in ROUGH (A,m1,n2) or z in ROUGH (A,n1,m2) )

assume A3: z in ROUGH (A,m1,n2) ; :: thesis: z in ROUGH (A,n1,m2)

then z in { x where x is Element of X : ( m1 <= #occurrences (x,A) & #occurrences (x,A) <= n2 ) } by Def25;

then consider a being Element of X such that

A4: ( z = a & m1 <= #occurrences (a,A) & #occurrences (a,A) <= n2 ) ;

( n1 <= #occurrences (a,A) & #occurrences (a,A) <= m2 ) by A1, A2, A4, XXREAL_0:2;

then z in { x where x is Element of X : ( n1 <= #occurrences (x,A) & #occurrences (x,A) <= m2 ) } by A4;

hence z in ROUGH (A,n1,m2) by A3, Def25; :: thesis: verum