set S = { (g * h) where g, h is Element of G : ( g in A & h in B ) } ;

{ (g * h) where g, h is Element of G : ( g in A & h in B ) } c= the carrier of G

{ (g * h) where g, h is Element of G : ( g in A & h in B ) } c= the carrier of G

proof

hence
{ (g * h) where g, h is Element of G : ( g in A & h in B ) } is Subset of G
; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (g * h) where g, h is Element of G : ( g in A & h in B ) } or x in the carrier of G )

assume x in { (g * h) where g, h is Element of G : ( g in A & h in B ) } ; :: thesis: x in the carrier of G

then ex g, h being Element of G st

( x = g * h & g in A & h in B ) ;

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

end;assume x in { (g * h) where g, h is Element of G : ( g in A & h in B ) } ; :: thesis: x in the carrier of G

then ex g, h being Element of G st

( x = g * h & g in A & h in B ) ;

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