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

{ x where x is Element of X : n <= #occurrences (x,A) } c= X

{ x where x is Element of X : n <= #occurrences (x,A) } c= X

proof

hence
{ x where x is Element of X : n <= #occurrences (x,A) } is List of X
; :: thesis: verum
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { x where x is Element of X : n <= #occurrences (x,A) } or z in X )

assume z in { x where x is Element of X : n <= #occurrences (x,A) } ; :: thesis: z in X

then ex x being Element of X st

( z = x & n <= #occurrences (x,A) ) ;

hence z in X by A1; :: thesis: verum

end;assume z in { x where x is Element of X : n <= #occurrences (x,A) } ; :: thesis: z in X

then ex x being Element of X st

( z = x & n <= #occurrences (x,A) ) ;

hence z in X by A1; :: thesis: verum