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

proof

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;

hence { x where x is Element of G : x * N meets A } is Subset of G ; :: thesis: verum