let G be Group; :: thesis: for F being non empty Subset of (Subgroups G) st (1). G in F holds
meet F = (1). G
let F be non empty Subset of (Subgroups G); :: thesis: ( (1). G in F implies meet F = (1). G )
assume A1: (1). G in F ; :: thesis: meet F = (1). G
reconsider 1G = (1). G as Element of Subgroups G by GROUP_3:def 1;
(carr G) . 1G = the carrier of ((1). G) by Def1;
then the carrier of ((1). G) in (carr G) .: F by A1, FUNCT_2:35;
then {(1_ G)} in (carr G) .: F by GROUP_2:def 7;
then meet ((carr G) .: F) c= {(1_ G)} by SETFAM_1:3;
then A2: the carrier of (meet F) c= {(1_ G)} by Def2;
(1). G is Subgroup of meet F by GROUP_2:65;
then the carrier of ((1). G) c= the carrier of (meet F) by GROUP_2:def 5;
then {(1_ G)} c= the carrier of (meet F) by GROUP_2:def 7;
then the carrier of (meet F) = {(1_ G)} by A2;
hence meet F = (1). G by GROUP_2:def 7; :: thesis: verum