let X be set ; :: thesis: for A being FinSequence of bool X st A <> {} holds
ROUGH (A,(len A)) = meet (rng A)
let A be FinSequence of bool X; :: thesis: ( A <> {} implies ROUGH (A,(len A)) = meet (rng A) )
assume A0: A <> {} ; :: thesis: ROUGH (A,(len A)) = meet (rng A)
thus ROUGH (A,(len A)) c= meet (rng A) :: according to XBOOLE_0:def 10 :: thesis: meet (rng A) c= ROUGH (A,(len A))

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in ROUGH (A,(len A)) or z in meet (rng A) )
assume z in ROUGH (A,(len A)) ; :: thesis: z in meet (rng A)
then z in { x where x is Element of X : len A <= #occurrences (x,A) } by ROUGH1;
then consider x being Element of X such that
A3: ( z = x & len A <= #occurrences (x,A) ) ;
#occurrences (x,A) <= len A by Th21;
hence z in meet (rng A) by A0, A3, Th22, XXREAL_0:1; :: thesis: verum

end;

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in meet (rng A) or z in ROUGH (A,(len A)) )
assume A2: z in meet (rng A) ; :: thesis: z in ROUGH (A,(len A))
then #occurrences (z,A) = len A by Th22;
then z in { x where x is Element of X : len A <= #occurrences (x,A) } by A2;
hence z in ROUGH (A,(len A)) by A2, ROUGH1; :: thesis: verum