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

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

proof

hence
{ e where e is Element of M : e is_dependent_on A } is Subset of M
; :: thesis: verum
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;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