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 A1: 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 object ; :: 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 Def24;
then consider x being Element of X such that
A2: ( z = x & len A <= #occurrences (x,A) ) ;
#occurrences (x,A) <= len A by Th54;
hence z in meet (rng A) by A1, A2, Th55, XXREAL_0:1; :: thesis: verum
end;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in meet (rng A) or z in ROUGH (A,(len A)) )
assume A3: z in meet (rng A) ; :: thesis: z in ROUGH (A,(len A))
then #occurrences (z,A) = len A by Th55;
then z in { x where x is Element of X : len A <= #occurrences (x,A) } by A3;
hence z in ROUGH (A,(len A)) by A3, Def24; :: thesis: verum