assume A2: X <> {} ; :: thesis: { x where x is Element of X : ( n <= #occurrences (x,A) & #occurrences (x,A) <= m ) } is List of X
{ x where x is Element of X : ( n <= #occurrences (x,A) & #occurrences (x,A) <= m ) } c= X

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { x where x is Element of X : ( n <= #occurrences (x,A) & #occurrences (x,A) <= m ) } or z in X )
assume z in { x where x is Element of X : ( n <= #occurrences (x,A) & #occurrences (x,A) <= m ) } ; :: thesis: z in X
then ex x being Element of X st
( z = x & n <= #occurrences (x,A) & #occurrences (x,A) <= m ) ;
hence z in X by A2; :: thesis: verum

end;

hence { x where x is Element of X : ( n <= #occurrences (x,A) & #occurrences (x,A) <= m ) } is List of X ; :: thesis: verum