1_ G in {(1_ G)} by TARSKI:def 1;
then reconsider PG = 1_ G as Element of ((1). G) by GROUP_2:def 7;
take PG ; :: according to GR_CY_1:def 7 :: thesis: multMagma(# the carrier of ((1). G), the multF of ((1). G) #) = gr {PG}
for G1 being Subgroup of (1). G st {PG} c= the carrier of G1 holds
(Omega). ((1). G) is Subgroup of G1

proof

let G1 be Subgroup of (1). G; :: thesis: ( {PG} c= the carrier of G1 implies (Omega). ((1). G) is Subgroup of G1 )
assume {PG} c= the carrier of G1 ; :: thesis: (Omega). ((1). G) is Subgroup of G1
then the carrier of ((Omega). ((1). G)) c= the carrier of G1 by GROUP_2:def 7;
hence (Omega). ((1). G) is Subgroup of G1 by GROUP_2:57; :: thesis: verum

end;

then for G1 being strict Subgroup of (1). G st {PG} c= the carrier of G1 holds
(Omega). ((1). G) is Subgroup of G1 ;
hence multMagma(# the carrier of ((1). G), the multF of ((1). G) #) = gr {PG} by GROUP_4:def 4; :: thesis: verum