set X = { e where e is Element of M : e is_dependent_on A } ;
{ e where e is Element of M : e is_dependent_on A } c= the carrier of M

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { e where e is Element of M : e is_dependent_on A } or x in the carrier of M )
assume x in { e where e is Element of M : e is_dependent_on A } ; :: thesis: x in the carrier of M
then ex e being Element of M st
( x = e & e is_dependent_on A ) ;
hence x in the carrier of M ; :: thesis: verum

end;

hence { e where e is Element of M : e is_dependent_on A } is Subset of M ; :: thesis: verum