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))

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

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 meet (rng A) or z in ROUGH (A,(len A)) )
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;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

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