now :: thesis: for x being object st x in { z where z is Element of E : for b being Element of E st b in B holds

z - b in A } holds

x in the carrier of E

hence
{ z where z is Element of E : for b being Element of E st b in B holds z - b in A } holds

x in the carrier of E

let x be object ; :: thesis: ( x in { z where z is Element of E : for b being Element of E st b in B holds

z - b in A } implies x in the carrier of E )

assume x in { z where z is Element of E : for b being Element of E st b in B holds

z - b in A } ; :: thesis: x in the carrier of E

then ex z being Element of E st

( x = z & ( for b being Element of E st b in B holds

z - b in A ) ) ;

hence x in the carrier of E ; :: thesis: verum

end;z - b in A } implies x in the carrier of E )

assume x in { z where z is Element of E : for b being Element of E st b in B holds

z - b in A } ; :: thesis: x in the carrier of E

then ex z being Element of E st

( x = z & ( for b being Element of E st b in B holds

z - b in A ) ) ;

hence x in the carrier of E ; :: thesis: verum

z - b in A } is binary-image of E by TARSKI:def 3; :: thesis: verum