reconsider h = 1 as Element of INT by INT_1:def 2;
reconsider h = h as Element of INT.Group ;
for G1 being Subgroup of INT.Group st {h} c= the carrier of G1 holds
(Omega). INT.Group is Subgroup of G1

h in {h} by TARSKI:def 1;
then reconsider h99 = h as Element of G1 by A1;
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume that
A2: x in the carrier of ((Omega). INT.Group) and
A3: not x in the carrier of G1 ; :: thesis:
reconsider x9 = x as Integer by A2;
( h99 |^ x9 in the carrier of G1 & h99 |^ x9 = h |^ x9 ) by GROUP_4:2;
hence contradiction by A3, Th16; :: thesis:

end;

end;