set X = { B where B is Subset of G : A,B are_conjugated } ;
{ B where B is Subset of G : A,B are_conjugated } c= bool the carrier of G

proof

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

end;

hence { B where B is Subset of G : A,B are_conjugated } is Subset-Family of G ; :: thesis: verum