set A = { j where j is Integer : i,j are_coprime } ;
{ j where j is Integer : i,j are_coprime } c= INT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { j where j is Integer : i,j are_coprime } or x in INT )
assume x in { j where j is Integer : i,j are_coprime } ; :: thesis: x in INT
then ex j being Integer st
( x = j & i,j are_coprime ) ;
hence x in INT by INT_1:def 2; :: thesis: verum

end;

hence { j where j is Integer : i,j are_coprime } is Subset of INT ; :: thesis: verum