let X be set ; 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; for A being FinSequence of bool X holds ROUGH (A,n,m) c= ROUGH (A,n)
let A be FinSequence of bool X; ROUGH (A,n,m) c= ROUGH (A,n)
let z be object ; TARSKI:def 3 ( not z in ROUGH (A,n,m) or z in ROUGH (A,n) )
assume A1:
z in ROUGH (A,n,m)
; 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; verum