assume A2:
the carrier of X <> {}
; :: thesis: { x where x is Element of X : ( card ((x ref) \ (rng A)) <= n & card ((rng A) \ (x ref)) <= m ) } is List of X

{ x where x is Element of X : ( card ((x ref) \ (rng A)) <= n & card ((rng A) \ (x ref)) <= m ) } c= the carrier of X

{ x where x is Element of X : ( card ((x ref) \ (rng A)) <= n & card ((rng A) \ (x ref)) <= m ) } c= the carrier of X

proof

hence
{ x where x is Element of X : ( card ((x ref) \ (rng A)) <= n & card ((rng A) \ (x ref)) <= m ) } 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 : ( card ((x ref) \ (rng A)) <= n & card ((rng A) \ (x ref)) <= m ) } or z in the carrier of X )

assume z in { x where x is Element of X : ( card ((x ref) \ (rng A)) <= n & card ((rng A) \ (x ref)) <= m ) } ; :: thesis: z in the carrier of X

then ex x being Element of X st

( z = x & card ((x ref) \ (rng A)) <= n & card ((rng A) \ (x ref)) <= m ) ;

hence z in the carrier of X by A2; :: thesis: verum

end;assume z in { x where x is Element of X : ( card ((x ref) \ (rng A)) <= n & card ((rng A) \ (x ref)) <= m ) } ; :: thesis: z in the carrier of X

then ex x being Element of X st

( z = x & card ((x ref) \ (rng A)) <= n & card ((rng A) \ (x ref)) <= m ) ;

hence z in the carrier of X by A2; :: thesis: verum