{ x where x is Element of G : x * N meets A } c= the carrier of G

proof

hence
{ x where x is Element of G : x * N meets A } is Subset of G
; :: thesis: verum
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is Element of G : x * N meets A } or y in the carrier of G )

assume y in { x where x is Element of G : x * N meets A } ; :: thesis: y in the carrier of G

then ex x being Element of G st

( y = x & x * N meets A ) ;

hence y in the carrier of G ; :: thesis: verum

end;assume y in { x where x is Element of G : x * N meets A } ; :: thesis: y in the carrier of G

then ex x being Element of G st

( y = x & x * N meets A ) ;

hence y in the carrier of G ; :: thesis: verum