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
reconsider H = h as strict Subgroup of G by GROUP_3:def 1;
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:59;
then A2: meet (Im ((carr G),h)) = (carr G) . h by SETFAM_1:10;
the carrier of (meet F) = meet ((carr G) .: F) by Def2;
then the carrier of (meet F) = the carrier of H by A1, A2, Def1;
hence meet F = h by GROUP_2:59; :: thesis: verum