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

proof

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

let x be set ; :: 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 x' = x as Integer by A2;
h in {h} by TARSKI:def 1;
then reconsider h'' = h as Element of G1 by A1;
A4: h'' |^ x' in the carrier of G1 ;
h'' |^ x' = h |^ x' by GROUP_4:4;
hence contradiction by A3, A4, Th39; :: thesis: verum

end;

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

end;

hence ( {h} c= the carrier of ((Omega). INT.Group ) & ( for G1 being strict Subgroup of INT.Group st {h} c= the carrier of G1 holds
(Omega). INT.Group is Subgroup of G1 ) ) ; :: thesis: verum

end;

hence INT.Group = gr {(@' 1)} by GROUP_4:def 5; :: thesis: verum