let G be Group; :: thesis: for h being Element of Subgroups G
for F being non empty Subset of (Subgroups G) st F = {h} holds
meet F = h
let h be Element of Subgroups G; :: thesis: for F being non empty Subset of (Subgroups G) st F = {h} holds
meet F = h
let F be non empty Subset of (Subgroups G); :: thesis: ( F = {h} implies meet F = h )
assume A1: F = {h} ; :: thesis: meet F = h
A2: the carrier of (meet F) = meet ((carr G) .: F) by Def2;
h in Subgroups G ;
then h in dom (carr G) by FUNCT_2:def 1;
then meet (Im (carr G),h) = meet {((carr G) . h)} by FUNCT_1:117;
then A3: meet (Im (carr G),h) = (carr G) . h by SETFAM_1:11;
reconsider H = h as strict Subgroup of G by GROUP_3:def 1;
the carrier of (meet F) = the carrier of H by A1, A2, A3, Def1;
hence meet F = h by GROUP_2:68; :: thesis: verum