{ x where x is Element of G : x * N c= carr H } c= the carrier of G

proof

hence
{ x where x is Element of G : x * N c= carr H } 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 c= carr H } or y in the carrier of G )

assume y in { x where x is Element of G : x * N c= carr H } ; :: thesis: y in the carrier of G

then ex x being Element of G st

( y = x & x * N c= carr H ) ;

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

end;assume y in { x where x is Element of G : x * N c= carr H } ; :: thesis: y in the carrier of G

then ex x being Element of G st

( y = x & x * N c= carr H ) ;

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