let X be set ; :: thesis: for n, m being Nat
for A being FinSequence of bool X st n <= m holds
ROUGH (A,m) c= ROUGH (A,n)
let n, m be Nat; :: thesis: for A being FinSequence of bool X st n <= m holds
ROUGH (A,m) c= ROUGH (A,n)
let A be FinSequence of bool X; :: thesis: ( n <= m implies ROUGH (A,m) c= ROUGH (A,n) )
assume A1: n <= m ; :: thesis: ROUGH (A,m) c= ROUGH (A,n)
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in ROUGH (A,m) or z in ROUGH (A,n) )
assume A2: z in ROUGH (A,m) ; :: thesis: z in ROUGH (A,n)
then z in { x where x is Element of X : m <= #occurrences (x,A) } by Def24;
then consider a being Element of X such that
A3: ( z = a & m <= #occurrences (a,A) ) ;
n <= #occurrences (a,A) by A1, A3, XXREAL_0:2;
then z in { x where x is Element of X : n <= #occurrences (x,A) } by A3;
hence z in ROUGH (A,n) by A2, Def24; :: thesis: verum