set F = { (g ") where g is Element of G : g in A } ;
{ (g ") where g is Element of G : g in A } c= the carrier of G

proof

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

end;

hence { (g ") where g is Element of G : g in A } is Subset of G ; :: thesis: verum