let G be Group; :: thesis: ( G is finite implies Subgroups G is finite )
defpred S₁[ set , set ] means ex H being strict Subgroup of G st
( $1 = H & $2 = the carrier of H );
assume A1: G is finite ; :: thesis: Subgroups G is finite
A2: for x being set st x in Subgroups G holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in Subgroups G implies ex y being set st S₁[x,y] )
assume x in Subgroups G ; :: thesis: ex y being set st S₁[x,y]
then reconsider F = x as strict Subgroup of G by Def1;
reconsider y = the carrier of F as set ;
take y ; :: thesis: S₁[x,y]
take F ; :: thesis: ( x = F & y = the carrier of F )
thus ( x = F & y = the carrier of F ) ; :: thesis: verum

end;

consider f being Function such that
A3: dom f = Subgroups G and
A4: for x being set st x in Subgroups G holds
S₁[x,f . x] from CLASSES1:sch 1(A2);
A5: rng f c= bool the carrier of G

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in bool the carrier of G )
assume x in rng f ; :: thesis: x in bool the carrier of G
then consider y being set such that
A6: ( y in dom f & f . y = x ) by FUNCT_1:def 5;
consider H being strict Subgroup of G such that
A7: ( y = H & x = the carrier of H ) by A3, A4, A6;
the carrier of H c= the carrier of G by GROUP_2:def 5;
hence x in bool the carrier of G by A7; :: thesis: verum

end;

f is one-to-one

proof

let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in dom f or not b₁ in dom f or not f . x = f . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A8: x in dom f and
A9: y in dom f and
A10: f . x = f . y ; :: thesis: x = y
A11: ex H1 being strict Subgroup of G st
( x = H1 & f . x = the carrier of H1 ) by A3, A4, A8;
ex H2 being strict Subgroup of G st
( y = H2 & f . y = the carrier of H2 ) by A3, A4, A9;
hence x = y by A10, A11, GROUP_2:68; :: thesis: verum

end;

then A12: card (Subgroups G) c= card (bool the carrier of G) by A3, A5, CARD_1:26;
the carrier of G is finite by A1;
then bool the carrier of G is finite ;
hence Subgroups G is finite by A12, CARD_2:68; :: thesis: verum