assume A1: the carrier of X <> {} ; :: thesis: { x where x is Element of X : rng A c= x ref } is List of X
{ x where x is Element of X : rng A c= x ref } c= the carrier of X

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { x where x is Element of X : rng A c= x ref } or z in the carrier of X )
assume z in { x where x is Element of X : rng A c= x ref } ; :: thesis: z in the carrier of X
then ex x being Element of X st
( z = x & rng A c= x ref ) ;
hence z in the carrier of X by A1; :: thesis: verum

end;

hence { x where x is Element of X : rng A c= x ref } is List of X ; :: thesis: verum