set S = { [x,y] where x, y is Element of G : y * (x ") in U } ;
{ [x,y] where x, y is Element of G : y * (x ") in U } c= [: the carrier of G, the carrier of G:]

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { [x,y] where x, y is Element of G : y * (x ") in U } or t in [: the carrier of G, the carrier of G:] )
assume t in { [x,y] where x, y is Element of G : y * (x ") in U } ; :: thesis: t in [: the carrier of G, the carrier of G:]
then ex x, y being Element of G st
( t = [x,y] & y * (x ") in U ) ;
hence t in [: the carrier of G, the carrier of G:] ; :: thesis: verum

end;

hence { [x,y] where x, y is Element of G : y * (x ") in U } is Subset of [: the carrier of G, the carrier of G:] ; :: thesis: verum