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

proof

let G1 be Subgroup of INT.Group ; :: thesis: ( {h} c= the carrier of G1 implies (Omega). INT.Group is Subgroup of G1 )
assume A1: {h} c= the carrier of G1 ; :: thesis: (Omega). INT.Group is Subgroup of G1
the carrier of ((Omega). INT.Group) c= the carrier of G1

proof

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: ( not x in the carrier of ((Omega). INT.Group) or x in the carrier of G1 )
assume that
A2: x in the carrier of ((Omega). INT.Group) and
A3: not x in the carrier of G1 ; :: thesis: contradiction
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: verum

end;

hence (Omega). INT.Group is Subgroup of G1 by GROUP_2:57; :: thesis: verum

end;

then for G1 being strict Subgroup of INT.Group st {h} c= the carrier of G1 holds
(Omega). INT.Group is Subgroup of G1 ;
hence INT.Group = gr {(@' 1)} by GROUP_4:def 4; :: thesis: verum