A1: (carr G) .: F <> {}

proof

consider x being Element of Subgroups G such that
A2: x in F by SUBSET_1:10;
(carr G) . x in (carr G) .: F by A2, FUNCT_2:43;
hence (carr G) .: F <> {} ; :: 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 A3: 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
A4: ( X1 in F & X = (carr G) . X1 ) by A3, FUNCT_2:116;
reconsider X1 = X1 as strict Subgroup of G by GROUP_3:def 1;
A5: X = the carrier of X1 by A4, Def1;
1_ G in X1 by GROUP_2:55;
hence 1_ G in X by A5, STRUCT_0:def 5; :: thesis: verum

end;

then A6: meet ((carr G) .: F) <> {} by A1, SETFAM_1:def 1;
A7: 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 A8: ( g1 in meet ((carr G) .: F) & 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

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

end;

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

end;

reconsider CG = (carr G) .: F as Subset-Family of G ;
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 A13: g in meet CG ; :: thesis: g " in meet CG
for X being set st X in (carr G) .: F holds
g " in X

proof

let X be set ; :: thesis: ( X in (carr G) .: F implies g " in X )
assume A14: X in (carr G) .: F ; :: thesis: g " in X
then A15: g in X by A13, SETFAM_1:def 1;
reconsider X = X as Subset of G by A14;
consider X1 being Element of Subgroups G such that
A16: ( X1 in F & X = (carr G) . X1 ) by A14, FUNCT_2:116;
reconsider X1 = X1 as strict Subgroup of G by GROUP_3:def 1;
A17: X = the carrier of X1 by A16, Def1;
reconsider h = g as Element of G ;
h in X1 by A15, A17, STRUCT_0:def 5;
then h " in X1 by GROUP_2:60;
hence g " in X by A17, STRUCT_0:def 5; :: thesis: verum

end;

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

end;

hence ex b₁ being strict Subgroup of G st the carrier of b₁ = meet ((carr G) .: F) by A6, A7, GROUP_2:61; :: thesis: verum