reconsider CG = (carr G) .: F as Subset-Family of G ;
A1: (carr G) .: F <> {}

proof

consider x being Element of Subgroups G such that
A2: x in F by SUBSET_1:4;
(carr G) . x in (carr G) .: F by A2, FUNCT_2:35;
hence (carr G) .: F <> {} ; :: thesis: verum

end;

A3: for g being Element of G st g in meet CG holds
g " in meet CG

proof

let g be Element of G; :: thesis: ( g in meet CG implies g " in meet CG )
assume A4: g in meet CG ; :: thesis: g " in meet CG
for X being set st X in (carr G) .: F holds
g " in X

proof

reconsider h = g as Element of G ;
let X be set ; :: thesis: ( X in (carr G) .: F implies g " in X )
assume A5: X in (carr G) .: F ; :: thesis: g " in X
then A6: g in X by A4, SETFAM_1:def 1;
reconsider X = X as Subset of G by A5;
consider X1 being Element of Subgroups G such that
X1 in F and
A7: X = (carr G) . X1 by A5, FUNCT_2:65;
reconsider X1 = X1 as strict Subgroup of G by GROUP_3:def 1;
A8: X = the carrier of X1 by A7, Def1;
then h in X1 by A6, STRUCT_0:def 5;
then h " in X1 by GROUP_2:51;
hence g " in X by A8, STRUCT_0:def 5; :: thesis: verum

end;

hence g " in meet CG by A1, SETFAM_1:def 1; :: thesis: verum

end;

A9: for g1, g2 being Element of G st g1 in meet ((carr G) .: F) & g2 in meet ((carr G) .: F) holds
g1 * g2 in meet ((carr G) .: F)

proof

let g1, g2 be Element of G; :: thesis: ( g1 in meet ((carr G) .: F) & g2 in meet ((carr G) .: F) implies g1 * g2 in meet ((carr G) .: F) )
assume that
A10: g1 in meet ((carr G) .: F) and
A11: g2 in meet ((carr G) .: F) ; :: thesis: g1 * g2 in meet ((carr G) .: F)
for X being set st X in (carr G) .: F holds
g1 * g2 in X

proof

reconsider h1 = g1, h2 = g2 as Element of G ;
let X be set ; :: thesis: ( X in (carr G) .: F implies g1 * g2 in X )
assume A12: X in (carr G) .: F ; :: thesis: g1 * g2 in X
then A13: g1 in X by A10, SETFAM_1:def 1;
A14: g2 in X by A11, A12, SETFAM_1:def 1;
reconsider X = X as Subset of G by A12;
consider X1 being Element of Subgroups G such that
X1 in F and
A15: X = (carr G) . X1 by A12, FUNCT_2:65;
reconsider X1 = X1 as strict Subgroup of G by GROUP_3:def 1;
A16: X = the carrier of X1 by A15, Def1;
then A17: h2 in X1 by A14, STRUCT_0:def 5;
h1 in X1 by A13, A16, STRUCT_0:def 5;
then h1 * h2 in X1 by A17, GROUP_2:50;
hence g1 * g2 in X by A16, STRUCT_0:def 5; :: thesis: verum

end;

hence g1 * g2 in meet ((carr G) .: F) by A1, SETFAM_1:def 1; :: thesis: verum

end;

for X being set st X in (carr G) .: F holds
1_ G in X

proof

let X be set ; :: thesis: ( X in (carr G) .: F implies 1_ G in X )
assume A18: X in (carr G) .: F ; :: thesis: 1_ G in X
then reconsider X = X as Subset of G ;
consider X1 being Element of Subgroups G such that
X1 in F and
A19: X = (carr G) . X1 by A18, FUNCT_2:65;
reconsider X1 = X1 as strict Subgroup of G by GROUP_3:def 1;
A20: 1_ G in X1 by GROUP_2:46;
X = the carrier of X1 by A19, Def1;
hence 1_ G in X by A20, STRUCT_0:def 5; :: thesis: verum

end;

then meet ((carr G) .: F) <> {} by A1, SETFAM_1:def 1;
hence ex b₁ being strict Subgroup of G st the carrier of b₁ = meet ((carr G) .: F) by A9, A3, GROUP_2:52; :: thesis: verum