let X be set ; :: thesis: for n, m being Nat

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

let n, m be Nat; :: thesis: for A being FinSequence of bool X holds ROUGH (A,n,m) c= ROUGH (A,n)

let A be FinSequence of bool X; :: thesis: ROUGH (A,n,m) c= ROUGH (A,n)

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in ROUGH (A,n,m) or z in ROUGH (A,n) )

assume A1: z in ROUGH (A,n,m) ; :: thesis: z in ROUGH (A,n)

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

then ex x being Element of X st

( z = x & n <= #occurrences (x,A) & #occurrences (x,A) <= m ) ;

then z in { x where x is Element of X : n <= #occurrences (x,A) } ;

hence z in ROUGH (A,n) by A1, Def24; :: thesis: verum

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

let n, m be Nat; :: thesis: for A being FinSequence of bool X holds ROUGH (A,n,m) c= ROUGH (A,n)

let A be FinSequence of bool X; :: thesis: ROUGH (A,n,m) c= ROUGH (A,n)

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in ROUGH (A,n,m) or z in ROUGH (A,n) )

assume A1: z in ROUGH (A,n,m) ; :: thesis: z in ROUGH (A,n)

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

then ex x being Element of X st

( z = x & n <= #occurrences (x,A) & #occurrences (x,A) <= m ) ;

then z in { x where x is Element of X : n <= #occurrences (x,A) } ;

hence z in ROUGH (A,n) by A1, Def24; :: thesis: verum