{ x where x is Element of G : x * N meets carr H } 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 carr H } or y in the carrier of G )
assume y in { x where x is Element of G : x * N meets carr H } ; :: thesis: y in the carrier of G
then ex x being Element of G st
( y = x & x * N meets carr H ) ;
hence y in the carrier of G ; :: thesis: verum

end;

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