:: On the Lattice of Subgroups of a Group
::  by Janusz Ganczarski
::
:: Received May 23, 1995
:: Copyright (c) 1995-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies GROUP_1, GROUP_2, STRUCT_0, XBOOLE_0, GROUP_3, SUBSET_1, GROUP_4,
      EQREL_1, TARSKI, GROUP_6, RELAT_1, FUNCT_1, ZFMISC_1, SETFAM_1, RLSUB_2,
      LATTICES, PBOOLE, REWRITE1, LATTICE3, VECTSP_8;
 notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, SETFAM_1, RELAT_1, RELSET_1,
      PARTFUN1, FUNCT_2, BINOP_1, STRUCT_0, ALGSTR_0, LATTICES, GROUP_1,
      GROUP_2, GROUP_3, GROUP_4, GROUP_6, LATTICE3, LATTICE4, VECTSP_8;
 constructors BINOP_1, REALSET1, GROUP_4, GROUP_6, LATTICE3, LATTICE4,
      VECTSP_8, RELSET_1;
 registrations SUBSET_1, FUNCT_1, FUNCT_2, STRUCT_0, LATTICES, GROUP_3,
      GROUP_4, RELSET_1;
 requirements BOOLE, SUBSET;
 definitions TARSKI, LATTICE3, VECTSP_8, XBOOLE_0;
 equalities XBOOLE_0, RELAT_1, GROUP_4;
 expansions TARSKI, LATTICE3, XBOOLE_0;
 theorems TARSKI, FUNCT_1, SUBSET_1, SETFAM_1, FUNCT_2, LATTICES, GROUP_2,
      GROUP_3, GROUP_4, GROUP_6, VECTSP_8, RELAT_1, XBOOLE_0, XBOOLE_1,
      STRUCT_0, LATTICE4;
 schemes FUNCT_2;

begin

theorem Th1:
  for G being Group for H1, H2 being Subgroup of G holds the
  carrier of H1 /\ H2 = (the carrier of H1) /\ the carrier of H2
proof
  let G be Group;
  let H1, H2 be Subgroup of G;
  the carrier of H2 = carr H2 by GROUP_2:def 9;
  then (the carrier of H1) /\ the carrier of H2 = carr H1 /\ carr H2 by
GROUP_2:def 9;
  hence thesis by GROUP_2:def 10;
end;

theorem Th2:
  for G being Group for h being set holds h in Subgroups G iff ex H
  being strict Subgroup of G st h = H
proof
  let G be Group;
  let h be set;
  thus h in Subgroups G implies ex H being strict Subgroup of G st h = H
  proof
    assume h in Subgroups G;
    then h is strict Subgroup of G by GROUP_3:def 1;
    hence thesis;
  end;
  thus thesis by GROUP_3:def 1;
end;

theorem Th3:
  for G being Group for A being Subset of G for H being strict
  Subgroup of G st A = the carrier of H holds gr A = H
proof
  let G be Group;
  let A be Subset of G;
  let H be strict Subgroup of G such that
A1: A = the carrier of H;
  gr carr H = H by GROUP_4:31;
  hence thesis by A1,GROUP_2:def 9;
end;

theorem Th4:
  for G being Group for H1, H2 being Subgroup of G for A being
Subset of G st A = (the carrier of H1) \/ the carrier of H2 holds H1 "\/" H2 =
  gr A
proof
  let G be Group;
  let H1, H2 be Subgroup of G;
A1: the carrier of H2 = carr H2 by GROUP_2:def 9;
  let A be Subset of G;
  assume A = (the carrier of H1) \/ the carrier of H2;
  hence thesis by A1,GROUP_2:def 9;
end;

theorem Th5:
  for G being Group for H1, H2 being Subgroup of G for g being
  Element of G holds g in H1 or g in H2 implies g in H1 "\/" H2
proof
  let G be Group;
  let H1, H2 be Subgroup of G;
  let g be Element of G;
  assume
A1: g in H1 or g in H2;
  now
    per cases by A1;
    suppose
A2:   g in H1;
      the carrier of H1 c= the carrier of G & the carrier of H2 c= the
      carrier of G by GROUP_2:def 5;
      then reconsider
      A = (the carrier of H1) \/ the carrier of H2 as Subset of G
      by XBOOLE_1:8;
      g in the carrier of H1 by A2,STRUCT_0:def 5;
      then g in A by XBOOLE_0:def 3;
      then g in gr A by GROUP_4:29;
      hence thesis by Th4;
    end;
    suppose
A3:   g in H2;
      the carrier of H1 c= the carrier of G & the carrier of H2 c= the
      carrier of G by GROUP_2:def 5;
      then reconsider
      A = (the carrier of H1) \/ the carrier of H2 as Subset of G
      by XBOOLE_1:8;
      g in the carrier of H2 by A3,STRUCT_0:def 5;
      then g in A by XBOOLE_0:def 3;
      then g in gr A by GROUP_4:29;
      hence thesis by Th4;
    end;
  end;
  hence thesis;
end;

theorem
  for G1, G2 being Group for f being Homomorphism of G1, G2 for H1 being
Subgroup of G1 holds ex H2 being strict Subgroup of G2 st the carrier of H2 = f
  .:the carrier of H1
proof
  let G1, G2 be Group;
  let f be Homomorphism of G1, G2;
  let H1 be Subgroup of G1;
  reconsider y = f.1_G1 as Element of G2;
A1: for g being Element of G2 st g in f.:the carrier of H1 holds g" in f.:
  the carrier of H1
  proof
    let g be Element of G2;
    assume g in f.:the carrier of H1;
    then consider x being Element of G1 such that
A2: x in the carrier of H1 and
A3: g = f.x by FUNCT_2:65;
    x in H1 by A2,STRUCT_0:def 5;
    then x" in H1 by GROUP_2:51;
    then
A4: x" in the carrier of H1 by STRUCT_0:def 5;
    f.x" = (f.x)" by GROUP_6:32;
    hence thesis by A3,A4,FUNCT_2:35;
  end;
A5: for g1, g2 being Element of G2 st g1 in f.:the carrier of H1 & g2 in f
  .:the carrier of H1 holds g1 * g2 in f.:the carrier of H1
  proof
    let g1, g2 be Element of G2;
    assume that
A6: g1 in f.:the carrier of H1 and
A7: g2 in f.:the carrier of H1;
    consider x being Element of G1 such that
A8: x in the carrier of H1 and
A9: g1 = f.x by A6,FUNCT_2:65;
    consider y being Element of G1 such that
A10: y in the carrier of H1 and
A11: g2 = f.y by A7,FUNCT_2:65;
A12: y in H1 by A10,STRUCT_0:def 5;
    x in H1 by A8,STRUCT_0:def 5;
    then x * y in H1 by A12,GROUP_2:50;
    then
A13: x * y in the carrier of H1 by STRUCT_0:def 5;
    f.(x * y) = f.x * f.y by GROUP_6:def 6;
    hence thesis by A9,A11,A13,FUNCT_2:35;
  end;
  1_G1 in H1 by GROUP_2:46;
  then dom f = the carrier of G1 & 1_G1 in the carrier of H1 by FUNCT_2:def 1
,STRUCT_0:def 5;
  then y in f.:the carrier of H1 by FUNCT_1:def 6;
  then consider H2 being strict Subgroup of G2 such that
A14: the carrier of H2 = f.:the carrier of H1 by A1,A5,GROUP_2:52;
  take H2;
  thus thesis by A14;
end;

theorem
  for G1, G2 being Group for f being Homomorphism of G1, G2 for H2 being
  Subgroup of G2 ex H1 being strict Subgroup of G1 st the carrier of H1 = f"the
  carrier of H2
proof
  let G1, G2 be Group;
  let f be Homomorphism of G1, G2;
  let H2 be Subgroup of G2;
A1: for g being Element of G1 st g in f"the carrier of H2 holds g" in f"the
  carrier of H2
  proof
    let g be Element of G1;
    assume g in f"the carrier of H2;
    then f.g in the carrier of H2 by FUNCT_2:38;
    then f.g in H2 by STRUCT_0:def 5;
    then (f.g)" in H2 by GROUP_2:51;
    then f.g" in H2 by GROUP_6:32;
    then f.g" in the carrier of H2 by STRUCT_0:def 5;
    hence thesis by FUNCT_2:38;
  end;
A2: for g1, g2 being Element of G1 st g1 in f"the carrier of H2 & g2 in f"
  the carrier of H2 holds g1 * g2 in f"the carrier of H2
  proof
    let g1, g2 be Element of G1;
    assume that
A3: g1 in f"the carrier of H2 and
A4: g2 in f"the carrier of H2;
    f.g2 in the carrier of H2 by A4,FUNCT_2:38;
    then
A5: f.g2 in H2 by STRUCT_0:def 5;
    f.g1 in the carrier of H2 by A3,FUNCT_2:38;
    then f.g1 in H2 by STRUCT_0:def 5;
    then f.g1 * f.g2 in H2 by A5,GROUP_2:50;
    then f.(g1 * g2) in H2 by GROUP_6:def 6;
    then f.(g1 * g2) in the carrier of H2 by STRUCT_0:def 5;
    hence thesis by FUNCT_2:38;
  end;
  1_G2 in H2 by GROUP_2:46;
  then 1_G2 in the carrier of H2 by STRUCT_0:def 5;
  then f.1_G1 in the carrier of H2 by GROUP_6:31;
  then f"the carrier of H2 <> {} by FUNCT_2:38;
  then consider H1 being strict Subgroup of G1 such that
A6: the carrier of H1 = f"the carrier of H2 by A1,A2,GROUP_2:52;
  take H1;
  thus thesis by A6;
end;

theorem
  for G1, G2 being Group for f being Homomorphism of G1, G2 for H1, H2
being Subgroup of G1 for H3, H4 being Subgroup of G2 st the carrier of H3 = f.:
  the carrier of H1 & the carrier of H4 = f.:the carrier of H2 holds H1 is
  Subgroup of H2 implies H3 is Subgroup of H4
proof
  let G1, G2 be Group;
  let f be Homomorphism of G1, G2;
  let H1, H2 be Subgroup of G1;
  let H3, H4 be Subgroup of G2 such that
A1: the carrier of H3 = f.:the carrier of H1 & the carrier of H4 = f.:
  the carrier of H2;
  assume H1 is Subgroup of H2;
  then the carrier of H1 c= the carrier of H2 by GROUP_2:def 5;
  hence thesis by A1,GROUP_2:57,RELAT_1:123;
end;

theorem
  for G1, G2 being Group for f being Homomorphism of G1, G2 for H1, H2
being Subgroup of G2 for H3, H4 being Subgroup of G1 st the carrier of H3 = f"
  the carrier of H1 & the carrier of H4 = f"the carrier of H2 holds H1 is
  Subgroup of H2 implies H3 is Subgroup of H4
proof
  let G1, G2 be Group;
  let f be Homomorphism of G1, G2;
  let H1, H2 be Subgroup of G2;
  let H3, H4 be Subgroup of G1 such that
A1: the carrier of H3 = f"the carrier of H1 & the carrier of H4 = f"the
  carrier of H2;
  assume H1 is Subgroup of H2;
  then the carrier of H1 c= the carrier of H2 by GROUP_2:def 5;
  hence thesis by A1,GROUP_2:57,RELAT_1:143;
end;

theorem
  for G1, G2 being Group for f being Function of the carrier of G1, the
  carrier of G2 for A being Subset of G1 holds f.:A c= f.:the carrier of gr A
proof
  let G1, G2 be Group;
  let f be Function of the carrier of G1, the carrier of G2;
  let A be Subset of G1;
  A c= the carrier of gr A by GROUP_4:def 4;
  hence thesis by RELAT_1:123;
end;

theorem
  for G1, G2 being Group for H1, H2 being Subgroup of G1 for f being
Function of the carrier of G1, the carrier of G2 for A being Subset of G1 st A
= (the carrier of H1) \/ the carrier of H2 holds f.:the carrier of H1 "\/" H2 =
  f.:the carrier of gr A by Th4;

theorem Th12:
  for G being Group for A being Subset of G st A = {1_G} holds gr A = (1).G
proof
  let G be Group;
  let A be Subset of G;
  assume A = {1_G};
  then A = the carrier of (1).G by GROUP_2:def 7;
  hence thesis by Th3;
end;

definition
  let G be Group;
  func carr G -> Function of Subgroups G, bool the carrier of G means
  :Def1:
  for H being strict Subgroup of G holds it.H = the carrier of H;
  existence
  proof
    defpred P [object, object] means
     for h being strict Subgroup of G st h = $1
    holds $2 = the carrier of h;
A1: for e being object st e in Subgroups G
     ex u being object st u in bool the carrier of G & P [e,u]
    proof
      let e be object;
      assume e in Subgroups G;
      then reconsider E = e as strict Subgroup of G by GROUP_3:def 1;
      reconsider u = carr E as Subset of G;
      take u;
      thus thesis by GROUP_2:def 9;
    end;
    consider f being Function of Subgroups G, bool the carrier of G such that
A2: for e being object st e in Subgroups G holds P [e,f.e] from FUNCT_2:
    sch 1 (A1);
    take f;
    let H be strict Subgroup of G;
    H in Subgroups G by GROUP_3:def 1;
    hence thesis by A2;
  end;
  uniqueness
  proof
    let F1, F2 be Function of Subgroups G, bool the carrier of G such that
A3: for H1 being strict Subgroup of G holds F1.H1 = the carrier of H1 and
A4: for H2 being strict Subgroup of G holds F2.H2 = the carrier of H2;
    for h being object st h in Subgroups G holds F1.h = F2.h
    proof
      let h be object;
      assume h in Subgroups G;
      then reconsider H = h as strict Subgroup of G by GROUP_3:def 1;
      thus F1.h = the carrier of H by A3
        .= F2.h by A4;
    end;
    hence thesis by FUNCT_2:12;
  end;
end;

theorem Th13:
  for G being Group for H being strict Subgroup of G for x being
  Element of G holds x in carr G.H iff x in H
proof
  let G be Group;
  let H be strict Subgroup of G;
  let x be Element of G;
  thus x in carr G.H implies x in H
  proof
    assume x in carr G.H;
    then x in the carrier of H by Def1;
    hence thesis by STRUCT_0:def 5;
  end;
  assume
A1: x in H;
  carr G.H = the carrier of H by Def1;
  hence thesis by A1,STRUCT_0:def 5;
end;

theorem
  for G being Group for H being strict Subgroup of G holds 1_G in carr G .H
proof
  let G be Group;
  let H be strict Subgroup of G;
  carr G.H = the carrier of H & 1_H = 1_G by Def1,GROUP_2:44;
  hence thesis;
end;

theorem
  for G being Group for H being strict Subgroup of G holds carr G.H <>
  {} by Def1;

theorem
  for G being Group for H being strict Subgroup of G for g1, g2 being
Element of G holds g1 in carr G.H & g2 in carr G.H implies g1 * g2 in carr G.H
proof
  let G be Group;
  let H be strict Subgroup of G;
  let g1, g2 be Element of G;
  assume g1 in carr G.H & g2 in carr G.H;
  then g1 in H & g2 in H by Th13;
  then g1 * g2 in H by GROUP_2:50;
  hence thesis by Th13;
end;

theorem
  for G being Group for H being strict Subgroup of G for g being Element
  of G holds g in carr G.H implies g" in carr G.H
proof
  let G be Group;
  let H be strict Subgroup of G;
  let g be Element of G;
  assume g in carr G.H;
  then g in H by Th13;
  then g" in H by GROUP_2:51;
  hence thesis by Th13;
end;

theorem Th18:
  for G being Group for H1, H2 being strict Subgroup of G holds
  the carrier of H1 /\ H2 = carr G.H1 /\ carr G.H2
proof
  let G be Group;
  let H1, H2 be strict Subgroup of G;
  carr G.H1 = the carrier of H1 & carr G.H2 = the carrier of H2 by Def1;
  hence thesis by Th1;
end;

theorem
  for G being Group for H1, H2 being strict Subgroup of G holds carr G.(
  H1 /\ H2) = carr G.H1 /\ carr G.H2
proof
  let G be Group;
  let H1, H2 be strict Subgroup of G;
  carr G.H1 /\ carr G.H2 = the carrier of H1 /\ H2 by Th18;
  hence thesis by Def1;
end;

definition
  let G be Group;
  let F be non empty Subset of Subgroups G;
  func meet F -> strict Subgroup of G means
  :Def2:
  the carrier of it = meet ( carr G.:F);
  existence
  proof
    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 thesis;
    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 such that
A4:   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;
        assume
A5:     X in carr G.:F;
        then
A6:     g in X by A4,SETFAM_1:def 1;
        reconsider 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 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 thesis by A8,STRUCT_0:def 5;
      end;
      hence thesis by A1,SETFAM_1:def 1;
    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 such that
A10:  g1 in meet (carr G.:F) and
A11:  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;
        assume
A12:    X in carr G.:F;
        then
A13:    g1 in X by A10,SETFAM_1:def 1;
A14:    g2 in X by A11,A12,SETFAM_1:def 1;
        reconsider 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 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 thesis by A16,STRUCT_0:def 5;
      end;
      hence thesis by A1,SETFAM_1:def 1;
    end;
    for X being set st X in carr G.:F holds 1_G in X
    proof
      let X be set;
      assume
A18:  X in carr G.:F;
      then reconsider 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 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 thesis by A20,STRUCT_0:def 5;
    end;
    then meet (carr G.:F) <> {} by A1,SETFAM_1:def 1;
    hence thesis by A9,A3,GROUP_2:52;
  end;
  uniqueness by GROUP_2:59;
end;

theorem
  for G being Group for F being non empty Subset of Subgroups G holds
  (1).G in F implies meet F = (1).G
proof
  let G be Group;
  let F be non empty Subset of Subgroups G;
  assume
A1: (1).G in F;
  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 thesis by GROUP_2:def 7;
end;

theorem
  for G being Group for h being Element of Subgroups G for F being non
  empty Subset of Subgroups G st F = { h } holds meet F = h
proof
  let G be Group;
  let h be Element of Subgroups G;
  let F be non empty Subset of Subgroups G such that
A1: 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 thesis by GROUP_2:59;
end;

theorem Th22:
  for G being Group for H1, H2 being Subgroup of G for h1, h2
  being Element of lattice G st h1 = H1 & h2 = H2 holds h1 "\/" h2 = H1 "\/" H2
proof
  let G be Group;
  let H1, H2 be Subgroup of G;
  let h1, h2 be Element of lattice G;
A1: h1 "\/" h2 = SubJoin G.(h1,h2) by LATTICES:def 1;
  assume
A2: h1 = H1 & h2 = H2;
  then H1 is strict & H2 is strict by GROUP_3:def 1;
  hence thesis by A2,A1,GROUP_4:def 10;
end;

theorem Th23:
  for G being Group for H1, H2 being Subgroup of G for h1, h2
  being Element of lattice G st h1 = H1 & h2 = H2 holds h1 "/\" h2 = H1 /\ H2
proof
  let G be Group;
  let H1, H2 be Subgroup of G;
  let h1, h2 be Element of lattice G;
A1: h1 "/\" h2 = SubMeet G.(h1,h2) by LATTICES:def 2;
  assume
A2: h1 = H1 & h2 = H2;
  then H1 is strict & H2 is strict by GROUP_3:def 1;
  hence thesis by A2,A1,GROUP_4:def 11;
end;

theorem
  for G being Group for p being Element of lattice G for H being
  Subgroup of G st p = H holds H is strict Subgroup of G by GROUP_3:def 1;

theorem Th25:
  for G being Group for H1, H2 being Subgroup of G for p, q being
  Element of lattice G st p = H1 & q = H2 holds p [= q iff the carrier of H1 c=
  the carrier of H2
proof
  let G be Group;
  let H1, H2 be Subgroup of G;
  let p, q be Element of lattice G such that
A1: p = H1 and
A2: q = H2;
A3: H1 is strict Subgroup of G by A1,GROUP_3:def 1;
A4: H2 is strict Subgroup of G by A2,GROUP_3:def 1;
  thus p [= q implies the carrier of H1 c= the carrier of H2
  proof
    assume p [= q;
    then
A5: p "/\" q = p by LATTICES:4;
    p "/\" q = (the L_meet of lattice G).(p,q) by LATTICES:def 2
      .= H1 /\ H2 by A1,A2,A3,A4,GROUP_4:def 11;
    then
    (the carrier of H1) /\ the carrier of H2 = the carrier of H1 by A1,A5,Th1;
    hence thesis by XBOOLE_1:17;
  end;
  thus the carrier of H1 c= the carrier of H2 implies p [= q
  proof
    assume the carrier of H1 c= the carrier of H2;
    then H1 is Subgroup of H2 by GROUP_2:57;
    then
A6: H1 /\ H2 = H1 by A3,GROUP_2:89;
    H1 /\ H2 = (the L_meet of lattice G).(p,q) by A1,A2,A3,A4,GROUP_4:def 11
      .= p "/\" q by LATTICES:def 2;
    hence thesis by A1,A6,LATTICES:4;
  end;
end;

theorem
  for G being Group for H1, H2 being Subgroup of G for p, q being
  Element of lattice G st p = H1 & q = H2 holds p [= q iff H1 is Subgroup of H2
proof
  let G be Group;
  let H1, H2 be Subgroup of G;
  let p, q be Element of lattice G;
  assume that
A1: p = H1 and
A2: q = H2;
  thus p [= q implies H1 is Subgroup of H2
  proof
    assume p [= q;
    then the carrier of H1 c= the carrier of H2 by A1,A2,Th25;
    hence thesis by GROUP_2:57;
  end;
A3: H1 is strict Subgroup of G by A1,GROUP_3:def 1;
A4: H2 is strict Subgroup of G by A2,GROUP_3:def 1;
  thus H1 is Subgroup of H2 implies p [= q
  proof
    assume H1 is Subgroup of H2;
    then
A5: H1 /\ H2 = H1 by A3,GROUP_2:89;
    H1 /\ H2 = (the L_meet of lattice G).(p,q) by A1,A2,A3,A4,GROUP_4:def 11
      .= p "/\" q by LATTICES:def 2;
    hence thesis by A1,A5,LATTICES:4;
  end;
end;

theorem
  for G being Group holds lattice G is complete
proof
  let G be Group;
  let Y be Subset of lattice G;
  per cases;
  suppose
A1: Y = {};
    take Top lattice G;
    thus Top lattice G is_less_than Y
    by A1;
    let b be Element of lattice G;
    assume b is_less_than Y;
    thus thesis by LATTICES:19;
  end;
  suppose
    Y <> {};
    then reconsider X = Y as non empty Subset of Subgroups G;
    reconsider p = meet X as Element of lattice G by GROUP_3:def 1;
    take p;
    set x = the Element of X;
    thus p is_less_than Y
    proof
      let q be Element of lattice G;
      reconsider H = q as strict Subgroup of G by GROUP_3:def 1;
      reconsider h = q as Element of Subgroups G;
      assume
A2:   q in Y;
      carr G.h = the carrier of H by Def1;
      then meet (carr G.:X) c= the carrier of H by A2,FUNCT_2:35,SETFAM_1:3;
      then the carrier of meet X c= the carrier of H by Def2;
      hence thesis by Th25;
    end;
    let r be Element of lattice G;
    reconsider H = r as Subgroup of G by GROUP_3:def 1;
    assume
A3: r is_less_than Y;
A4: for Z1 being set st Z1 in carr G.:X holds the carrier of H c= Z1
    proof
      let Z1 be set;
      assume
A5:   Z1 in carr G.:X;
      then reconsider Z2 = Z1 as Subset of G;
      consider z1 being Element of Subgroups G such that
A6:   z1 in X & Z2 = carr G.z1 by A5,FUNCT_2:65;
      reconsider z1 as Element of lattice G;
      reconsider z3 = z1 as strict Subgroup of G by GROUP_3:def 1;
      Z1 = the carrier of z3 & r [= z1 by A3,A6,Def1;
      hence thesis by Th25;
    end;
    carr G.x in carr G.:X by FUNCT_2:35;
    then the carrier of H c= meet (carr G.:X) by A4,SETFAM_1:5;
    then the carrier of H c= the carrier of meet X by Def2;
    hence thesis by Th25;
  end;
end;

definition
  let G1, G2 be Group;
  let f be Function of the carrier of G1, the carrier of G2;
  func FuncLatt f -> Function of the carrier of lattice G1, the carrier of
  lattice G2 means
  :Def3:
  for H being strict Subgroup of G1, A being Subset of G2
  st A = f.:the carrier of H holds it.H = gr A;
  existence
  proof
    defpred P [object, object] means
for H being strict Subgroup of G1 st H = $1 for
A being Subset of G2 st A = f.:the carrier of H holds $2 = gr (f.:the carrier
    of H);
A1: for e being object st e in the carrier of lattice G1
     ex u being object st u in the carrier of lattice G2 & P [e,u]
    proof
      let e be object;
      assume e in the carrier of lattice G1;
      then reconsider E = e as strict Subgroup of G1 by GROUP_3:def 1;
      reconsider u = gr (f.:the carrier of E) as strict Subgroup of G2;
      reconsider u as Element of lattice G2 by GROUP_3:def 1;
      take u;
      thus thesis;
    end;
    consider f1 being Function of the carrier of lattice G1, the carrier of
    lattice G2 such that
A2: for e being object st e in the carrier of lattice G1 holds P [e,f1.e]
    from FUNCT_2:sch 1 (A1);
    take f1;
    let H be strict Subgroup of G1;
    let A be Subset of G2;
A3: H in the carrier of lattice G1 by GROUP_3:def 1;
    assume A = f.:the carrier of H;
    hence thesis by A2,A3;
  end;
  uniqueness
  proof
    let f1, f2 be Function of the carrier of lattice G1, the carrier of
    lattice G2 such that
A4: for H being strict Subgroup of G1, A being Subset of G2 st A = f.:
    the carrier of H holds f1.H = gr A and
A5: for H being strict Subgroup of G1, A being Subset of G2 st A = f.:
    the carrier of H holds f2.H = gr A;
    for h being object st h in the carrier of lattice G1 holds f1.h = f2.h
    proof
      let h be object;
      assume h in the carrier of lattice G1;
      then reconsider H = h as strict Subgroup of G1 by GROUP_3:def 1;
      thus f1.h = gr (f.:the carrier of H) by A4
        .= f2.h by A5;
    end;
    hence thesis by FUNCT_2:12;
  end;
end;

theorem
  for G being Group holds FuncLatt id the carrier of G = id the carrier
  of lattice G
proof
  let G be Group;
  set f = id the carrier of G;
A1: for x being object st x in the carrier of lattice G
    holds (FuncLatt f).x = x
  proof
    let x be object;
    assume x in the carrier of lattice G;
    then reconsider x as strict Subgroup of G by GROUP_3:def 1;
A2: the carrier of x c= f.:the carrier of x
    proof
      let z be object;
      assume
A3:   z in the carrier of x;
      the carrier of x c= the carrier of G by GROUP_2:def 5;
      then reconsider z as Element of G by A3;
      f.z = z;
      hence thesis by A3,FUNCT_2:35;
    end;
A4: f.:the carrier of x c= the carrier of x
    proof
      let z be object;
      assume
A5:   z in f.:the carrier of x;
      then reconsider z as Element of G;
      ex Z being Element of G st Z in the carrier of x & z = f. Z by A5,
FUNCT_2:65;
      hence thesis;
    end;
    then reconsider X = the carrier of x as Subset of G by A2,XBOOLE_0:def 10;
    f.:the carrier of x = the carrier of x by A4,A2;
    then (FuncLatt f).x = gr X by Def3;
    hence thesis by Th3;
  end;
  dom FuncLatt f = the carrier of lattice G by FUNCT_2:def 1;
  hence thesis by A1,FUNCT_1:17;
end;

theorem
  for G1, G2 being Group for f being Homomorphism of G1, G2 st f is
  one-to-one holds FuncLatt f is one-to-one
proof
  let G1, G2 be Group;
  let f be Homomorphism of G1, G2 such that
A1: f is one-to-one;
  for x1, x2 being object st x1 in dom FuncLatt f & x2 in dom FuncLatt f & (
  FuncLatt f).x1 = (FuncLatt f).x2 holds x1 = x2
  proof
    reconsider y = f.(1_G1) as Element of G2;
    let x1, x2 be object;
    assume that
A2: x1 in dom FuncLatt f & x2 in dom FuncLatt f and
A3: (FuncLatt f).x1 = (FuncLatt f).x2;
    reconsider x1, x2 as strict Subgroup of G1 by A2,GROUP_3:def 1;
    reconsider A1 = f.:the carrier of x1, A2 = f.:the carrier of x2 as Subset
    of G2;
A4: for g being Element of G2 st g in f.:the carrier of x1 holds g" in f
    .:the carrier of x1
    proof
      let g be Element of G2;
      assume g in f.:the carrier of x1;
      then consider x being Element of G1 such that
A5:   x in the carrier of x1 and
A6:   g = f.x by FUNCT_2:65;
      x in x1 by A5,STRUCT_0:def 5;
      then x" in x1 by GROUP_2:51;
      then
A7:   x" in the carrier of x1 by STRUCT_0:def 5;
      f.x" = (f.x)" by GROUP_6:32;
      hence thesis by A6,A7,FUNCT_2:35;
    end;
A8: for g1, g2 being Element of G2 st g1 in f.:the carrier of x1 & g2 in
    f.:the carrier of x1 holds g1 * g2 in f.:the carrier of x1
    proof
      let g1, g2 be Element of G2;
      assume that
A9:   g1 in f.:the carrier of x1 and
A10:  g2 in f.:the carrier of x1;
      consider x being Element of G1 such that
A11:  x in the carrier of x1 and
A12:  g1 = f.x by A9,FUNCT_2:65;
      consider y being Element of G1 such that
A13:  y in the carrier of x1 and
A14:  g2 = f.y by A10,FUNCT_2:65;
A15:  y in x1 by A13,STRUCT_0:def 5;
      x in x1 by A11,STRUCT_0:def 5;
      then x * y in x1 by A15,GROUP_2:50;
      then
A16:  x * y in the carrier of x1 by STRUCT_0:def 5;
      f.(x * y) = f.x * f.y by GROUP_6:def 6;
      hence thesis by A12,A14,A16,FUNCT_2:35;
    end;
A17: for g being Element of G2 st g in f.:the carrier of x2 holds g" in f
    .:the carrier of x2
    proof
      let g be Element of G2;
      assume g in f.:the carrier of x2;
      then consider x being Element of G1 such that
A18:  x in the carrier of x2 and
A19:  g = f.x by FUNCT_2:65;
      x in x2 by A18,STRUCT_0:def 5;
      then x" in x2 by GROUP_2:51;
      then
A20:  x" in the carrier of x2 by STRUCT_0:def 5;
      f.x" = (f.x)" by GROUP_6:32;
      hence thesis by A19,A20,FUNCT_2:35;
    end;
A21: dom f = the carrier of G1 by FUNCT_2:def 1;
A22: for g1, g2 being Element of G2 st g1 in f.:the carrier of x2 & g2 in
    f.:the carrier of x2 holds g1 * g2 in f.:the carrier of x2
    proof
      let g1, g2 be Element of G2;
      assume that
A23:  g1 in f.:the carrier of x2 and
A24:  g2 in f.:the carrier of x2;
      consider x being Element of G1 such that
A25:  x in the carrier of x2 and
A26:  g1 = f.x by A23,FUNCT_2:65;
      consider y being Element of G1 such that
A27:  y in the carrier of x2 and
A28:  g2 = f.y by A24,FUNCT_2:65;
A29:  y in x2 by A27,STRUCT_0:def 5;
      x in x2 by A25,STRUCT_0:def 5;
      then x * y in x2 by A29,GROUP_2:50;
      then
A30:  x * y in the carrier of x2 by STRUCT_0:def 5;
      f.(x * y) = f.x * f.y by GROUP_6:def 6;
      hence thesis by A26,A28,A30,FUNCT_2:35;
    end;
    1_G1 in x2 by GROUP_2:46;
    then
A31: 1_G1 in the carrier of x2 by STRUCT_0:def 5;
A32: (FuncLatt f).x1 = gr A1 & (FuncLatt f).x2 = gr A2 by Def3;
    ex y being Element of G2 st y = f.(1_G1);
    then f.:the carrier of x2 <> {} by A21,A31,FUNCT_1:def 6;
    then consider B2 being strict Subgroup of G2 such that
A33: the carrier of B2 = f.:the carrier of x2 by A17,A22,GROUP_2:52;
    1_G1 in x1 by GROUP_2:46;
    then 1_G1 in the carrier of x1 by STRUCT_0:def 5;
    then y in f.:the carrier of x1 by A21,FUNCT_1:def 6;
    then
A34: ex B1 being strict Subgroup of G2 st the carrier of B1 = f .:the
    carrier of x1 by A4,A8,GROUP_2:52;
    gr (f.:the carrier of x2) = B2 by A33,Th3;
    then
A35: f.:the carrier of x1 = f.:the carrier of x2 by A3,A32,A34,A33,Th3;
    the carrier of x2 c= dom f by A21,GROUP_2:def 5;
    then
A36: the carrier of x2 c= the carrier of x1 by A1,A35,FUNCT_1:87;
    the carrier of x1 c= dom f by A21,GROUP_2:def 5;
    then the carrier of x1 c= the carrier of x2 by A1,A35,FUNCT_1:87;
    then the carrier of x1 = the carrier of x2 by A36;
    hence thesis by GROUP_2:59;
  end;
  hence thesis by FUNCT_1:def 4;
end;

theorem
  for G1, G2 being Group for f being Homomorphism of G1, G2 holds (
  FuncLatt f).(1).G1 = (1).G2
proof
  let G1, G2 be Group;
  let f be Homomorphism of G1, G2;
  consider A being Subset of G2 such that
A1: A = f.:the carrier of (1).G1;
A2: A = f.:{1_G1} by A1,GROUP_2:def 7;
A3: 1_G1 in {1_G1} & 1_G2 = f.1_G1 by GROUP_6:31,TARSKI:def 1;
  for x being object holds x in A iff x = 1_G2
  proof
    let x be object;
    thus x in A implies x = 1_G2
    proof
      assume
A4:   x in A;
      then reconsider x as Element of G2;
      consider y being Element of G1 such that
A5:   y in {1_G1} and
A6:   x = f.y by A2,A4,FUNCT_2:65;
      y = 1_G1 by A5,TARSKI:def 1;
      hence thesis by A6,GROUP_6:31;
    end;
    thus thesis by A2,A3,FUNCT_2:35;
  end;
  then A = {1_G2} by TARSKI:def 1;
  then gr A = (1).G2 by Th12;
  hence thesis by A1,Def3;
end;

theorem Th31:
  for G1, G2 being Group for f being Homomorphism of G1, G2 st f
  is one-to-one holds FuncLatt f is Semilattice-Homomorphism of lattice G1,
  lattice G2
proof
  let G1, G2 be Group;
  let f be Homomorphism of G1, G2 such that
A1: f is one-to-one;
  for a, b being Element of lattice G1 holds (FuncLatt f).(a "/\" b) = (
  FuncLatt f).a "/\" (FuncLatt f).b
  proof
    let a, b be Element of lattice G1;
    consider A1 being strict Subgroup of G1 such that
A2: A1 = a by Th2;
    consider B1 being strict Subgroup of G1 such that
A3: B1 = b by Th2;
    thus thesis
    proof
A4:   for g1, g2 being Element of G2 st g1 in f.:the carrier of B1 & g2
      in f.:the carrier of B1 holds g1 * g2 in f.:the carrier of B1
      proof
        let g1, g2 be Element of G2;
        assume that
A5:     g1 in f.:the carrier of B1 and
A6:     g2 in f.:the carrier of B1;
        consider x being Element of G1 such that
A7:     x in the carrier of B1 and
A8:     g1 = f.x by A5,FUNCT_2:65;
        consider y being Element of G1 such that
A9:     y in the carrier of B1 and
A10:    g2 = f.y by A6,FUNCT_2:65;
A11:    y in B1 by A9,STRUCT_0:def 5;
        x in B1 by A7,STRUCT_0:def 5;
        then x * y in B1 by A11,GROUP_2:50;
        then
A12:    x * y in the carrier of B1 by STRUCT_0:def 5;
        f.(x * y) = f.x * f.y by GROUP_6:def 6;
        hence thesis by A8,A10,A12,FUNCT_2:35;
      end;
A13:  for g being Element of G2 st g in f.:the carrier of B1 holds g" in
      f.:the carrier of B1
      proof
        let g be Element of G2;
        assume g in f.:the carrier of B1;
        then consider x being Element of G1 such that
A14:    x in the carrier of B1 and
A15:    g = f.x by FUNCT_2:65;
        x in B1 by A14,STRUCT_0:def 5;
        then x" in B1 by GROUP_2:51;
        then
A16:    x" in the carrier of B1 by STRUCT_0:def 5;
        f.x" = (f.x)" by GROUP_6:32;
        hence thesis by A15,A16,FUNCT_2:35;
      end;
A17:  for g being Element of G2 st g in f.:the carrier of A1 holds g" in
      f.:the carrier of A1
      proof
        let g be Element of G2;
        assume g in f.:the carrier of A1;
        then consider x being Element of G1 such that
A18:    x in the carrier of A1 and
A19:    g = f.x by FUNCT_2:65;
        x in A1 by A18,STRUCT_0:def 5;
        then x" in A1 by GROUP_2:51;
        then
A20:    x" in the carrier of A1 by STRUCT_0:def 5;
        f.x" = (f.x)" by GROUP_6:32;
        hence thesis by A19,A20,FUNCT_2:35;
      end;
      1_G1 in A1 by GROUP_2:46;
      then
A21:  1_G1 in the carrier of A1 by STRUCT_0:def 5;
A22:  (FuncLatt f).(A1 /\ B1) = gr (f.:the carrier of A1 /\ B1) by Def3;
      consider C1 being strict Subgroup of G1 such that
A23:  C1 = A1 /\ B1;
A24:  for g1, g2 being Element of G2 st g1 in f.:the carrier of A1 & g2
      in f.:the carrier of A1 holds g1 * g2 in f.:the carrier of A1
      proof
        let g1, g2 be Element of G2;
        assume that
A25:    g1 in f.:the carrier of A1 and
A26:    g2 in f.:the carrier of A1;
        consider x being Element of G1 such that
A27:    x in the carrier of A1 and
A28:    g1 = f.x by A25,FUNCT_2:65;
        consider y being Element of G1 such that
A29:    y in the carrier of A1 and
A30:    g2 = f.y by A26,FUNCT_2:65;
A31:    y in A1 by A29,STRUCT_0:def 5;
        x in A1 by A27,STRUCT_0:def 5;
        then x * y in A1 by A31,GROUP_2:50;
        then
A32:    x * y in the carrier of A1 by STRUCT_0:def 5;
        f.(x * y) = f.x * f.y by GROUP_6:def 6;
        hence thesis by A28,A30,A32,FUNCT_2:35;
      end;
      1_G1 in B1 by GROUP_2:46;
      then
A33:  1_G1 in the carrier of B1 by STRUCT_0:def 5;
A34:  (FuncLatt f).a = gr (f.:the carrier of A1) & (FuncLatt f).b = gr (f
      .:the carrier of B1) by A2,A3,Def3;
A35:  dom f = the carrier of G1 by FUNCT_2:def 1;
A36:  for g1, g2 being Element of G2 st g1 in f.:the carrier of C1 & g2
      in f.:the carrier of C1 holds g1 * g2 in f.:the carrier of C1
      proof
        let g1, g2 be Element of G2;
        assume that
A37:    g1 in f.:the carrier of C1 and
A38:    g2 in f.:the carrier of C1;
        consider x being Element of G1 such that
A39:    x in the carrier of C1 and
A40:    g1 = f.x by A37,FUNCT_2:65;
        consider y being Element of G1 such that
A41:    y in the carrier of C1 and
A42:    g2 = f.y by A38,FUNCT_2:65;
A43:    y in C1 by A41,STRUCT_0:def 5;
        x in C1 by A39,STRUCT_0:def 5;
        then x * y in C1 by A43,GROUP_2:50;
        then
A44:    x * y in the carrier of C1 by STRUCT_0:def 5;
        f.(x * y) = f.x * f.y by GROUP_6:def 6;
        hence thesis by A40,A42,A44,FUNCT_2:35;
      end;
A45:  for g being Element of G2 st g in f.:the carrier of C1 holds g" in
      f.:the carrier of C1
      proof
        let g be Element of G2;
        assume g in f.:the carrier of C1;
        then consider x being Element of G1 such that
A46:    x in the carrier of C1 and
A47:    g = f.x by FUNCT_2:65;
        x in C1 by A46,STRUCT_0:def 5;
        then x" in C1 by GROUP_2:51;
        then
A48:    x" in the carrier of C1 by STRUCT_0:def 5;
        f.x" = (f.x)" by GROUP_6:32;
        hence thesis by A47,A48,FUNCT_2:35;
      end;
      1_G1 in C1 by GROUP_2:46;
      then
A49:  1_G1 in the carrier of C1 by STRUCT_0:def 5;
      ex y2 being Element of G2 st y2 = f.1_G1;
      then f.:the carrier of C1 <> {} by A35,A49,FUNCT_1:def 6;
      then consider C3 being strict Subgroup of G2 such that
A50:  the carrier of C3 = f.:the carrier of C1 by A45,A36,GROUP_2:52;
      ex y1 being Element of G2 st y1 = f.1_G1;
      then f.:the carrier of B1 <> {} by A35,A33,FUNCT_1:def 6;
      then consider B3 being strict Subgroup of G2 such that
A51:  the carrier of B3 = f.:the carrier of B1 by A13,A4,GROUP_2:52;
      ex y being Element of G2 st y = f.1_G1;
      then f.:the carrier of A1 <> {} by A35,A21,FUNCT_1:def 6;
      then consider A3 being strict Subgroup of G2 such that
A52:  the carrier of A3 = f.:the carrier of A1 by A17,A24,GROUP_2:52;
A53:  the carrier of C3 c= the carrier of A3 /\ B3
      proof
A54:    f.:the carrier of A1 /\ B1 c= f.:the carrier of B1
        proof
          let x be object;
          assume
A55:      x in f.:the carrier of A1 /\ B1;
          then reconsider x as Element of G2;
          consider y being Element of G1 such that
A56:      y in the carrier of A1 /\ B1 and
A57:      x = f.y by A55,FUNCT_2:65;
          y in (the carrier of A1) /\ the carrier of B1 by A56,Th1;
          then y in the carrier of B1 by XBOOLE_0:def 4;
          hence thesis by A57,FUNCT_2:35;
        end;
A58:    f.:the carrier of A1 /\ B1 c= f.:the carrier of A1
        proof
          let x be object;
          assume
A59:      x in f.:the carrier of A1 /\ B1;
          then reconsider x as Element of G2;
          consider y being Element of G1 such that
A60:      y in the carrier of A1 /\ B1 and
A61:      x = f.y by A59,FUNCT_2:65;
          y in (the carrier of A1) /\ the carrier of B1 by A60,Th1;
          then y in the carrier of A1 by XBOOLE_0:def 4;
          hence thesis by A61,FUNCT_2:35;
        end;
        let x be object;
        assume
A62:    x in the carrier of C3;
        the carrier of C3 c= the carrier of G2 by GROUP_2:def 5;
        then reconsider x as Element of G2 by A62;
        consider y being Element of G1 such that
A63:    y in the carrier of A1 /\ B1 and
A64:    x = f.y by A23,A50,A62,FUNCT_2:65;
        f.y in f.:the carrier of A1 /\ B1 by A63,FUNCT_2:35;
        then f.y in (the carrier of A3) /\ the carrier of B3 by A52,A51,A58,A54
,XBOOLE_0:def 4;
        hence thesis by A64,Th1;
      end;
A65:  gr (f.:the carrier of B1) = B3 by A51,Th3;
      the carrier of A3 /\ B3 c= the carrier of C3
      proof
        let x be object;
        assume x in the carrier of A3 /\ B3;
        then x in (the carrier of A3) /\ the carrier of B3 by Th1;
        then
        x in f.:((the carrier of A1) /\ the carrier of B1) by A1,A52,A51,
FUNCT_1:62;
        hence thesis by A23,A50,Th1;
      end;
      then the carrier of A3 /\ B3 = the carrier of C3 by A53;
      then gr (f.:the carrier of A1 /\ B1) = A3 /\ B3 by A23,A50,Th3
        .= gr (f.:the carrier of A1) /\ gr (f.:the carrier of B1) by A52,A65
,Th3
        .= (FuncLatt f).a "/\" (FuncLatt f).b by A34,Th23;
      hence thesis by A2,A3,A22,Th23;
    end;
  end;
  hence thesis by LATTICE4:def 2;
end;

theorem Th32:
  for G1, G2 being Group for f being Homomorphism of G1, G2 holds
  FuncLatt f is sup-Semilattice-Homomorphism of lattice G1, lattice G2
proof
  let G1, G2 be Group;
  let f be Homomorphism of G1, G2;
  for a, b being Element of lattice G1 holds (FuncLatt f).(a "\/" b) = (
  FuncLatt f).a "\/" (FuncLatt f).b
  proof
    let a, b be Element of lattice G1;
    consider A1 being strict Subgroup of G1 such that
A1: A1 = a by Th2;
    consider B1 being strict Subgroup of G1 such that
A2: B1 = b by Th2;
    thus thesis
    proof
A3:   for g being Element of G2 st g in f.:the carrier of B1 holds g" in
      f.:the carrier of B1
      proof
        let g be Element of G2;
        assume g in f.:the carrier of B1;
        then consider x being Element of G1 such that
A4:     x in the carrier of B1 and
A5:     g = f.x by FUNCT_2:65;
        x in B1 by A4,STRUCT_0:def 5;
        then x" in B1 by GROUP_2:51;
        then
A6:     x" in the carrier of B1 by STRUCT_0:def 5;
        f.x" = (f.x)" by GROUP_6:32;
        hence thesis by A5,A6,FUNCT_2:35;
      end;
      1_G1 in A1 by GROUP_2:46;
      then
A7:   1_G1 in the carrier of A1 by STRUCT_0:def 5;
A8:   ex y being Element of G2 st y = f.1_G1;
      the carrier of A1 c= the carrier of G1 & the carrier of B1 c= the
      carrier of G1 by GROUP_2:def 5;
      then reconsider
      A = (the carrier of A1) \/ the carrier of B1 as Subset of G1
      by XBOOLE_1:8;
A9:   for g being Element of G2 st g in f.:the carrier of A1 holds g" in
      f.:the carrier of A1
      proof
        let g be Element of G2;
        assume g in f.:the carrier of A1;
        then consider x being Element of G1 such that
A10:    x in the carrier of A1 and
A11:    g = f.x by FUNCT_2:65;
        x in A1 by A10,STRUCT_0:def 5;
        then x" in A1 by GROUP_2:51;
        then
A12:    x" in the carrier of A1 by STRUCT_0:def 5;
        f.x" = (f.x)" by GROUP_6:32;
        hence thesis by A11,A12,FUNCT_2:35;
      end;
      reconsider B = (f.:the carrier of A1) \/ f.:the carrier of B1 as Subset
      of G2;
A13:  dom f = the carrier of G1 by FUNCT_2:def 1;
A14:  for g1, g2 being Element of G2 st g1 in f.:the carrier of B1 & g2
      in f.:the carrier of B1 holds g1 * g2 in f.:the carrier of B1
      proof
        let g1, g2 be Element of G2;
        assume that
A15:    g1 in f.:the carrier of B1 and
A16:    g2 in f.:the carrier of B1;
        consider x being Element of G1 such that
A17:    x in the carrier of B1 and
A18:    g1 = f.x by A15,FUNCT_2:65;
        consider y being Element of G1 such that
A19:    y in the carrier of B1 and
A20:    g2 = f.y by A16,FUNCT_2:65;
A21:    y in B1 by A19,STRUCT_0:def 5;
        x in B1 by A17,STRUCT_0:def 5;
        then x * y in B1 by A21,GROUP_2:50;
        then
A22:    x * y in the carrier of B1 by STRUCT_0:def 5;
        f.(x * y) = f.x * f.y by GROUP_6:def 6;
        hence thesis by A18,A20,A22,FUNCT_2:35;
      end;
      1_G1 in B1 by GROUP_2:46;
      then
A23:  1_G1 in the carrier of B1 by STRUCT_0:def 5;
A24:  (FuncLatt f).(A1 "\/" B1) = gr (f.:the carrier of A1 "\/" B1) by Def3;
      ex y1 being Element of G2 st y1 = f.1_G1;
      then f.:the carrier of B1 <> {} by A13,A23,FUNCT_1:def 6;
      then consider B3 being strict Subgroup of G2 such that
A25:  the carrier of B3 = f.:the carrier of B1 by A3,A14,GROUP_2:52;
A26:  for g1, g2 being Element of G2 st g1 in f.:the carrier of A1 & g2
      in f.:the carrier of A1 holds g1 * g2 in f.:the carrier of A1
      proof
        let g1, g2 be Element of G2;
        assume that
A27:    g1 in f.:the carrier of A1 and
A28:    g2 in f.:the carrier of A1;
        consider x being Element of G1 such that
A29:    x in the carrier of A1 and
A30:    g1 = f.x by A27,FUNCT_2:65;
        consider y being Element of G1 such that
A31:    y in the carrier of A1 and
A32:    g2 = f.y by A28,FUNCT_2:65;
A33:    y in A1 by A31,STRUCT_0:def 5;
        x in A1 by A29,STRUCT_0:def 5;
        then x * y in A1 by A33,GROUP_2:50;
        then
A34:    x * y in the carrier of A1 by STRUCT_0:def 5;
        f.(x * y) = f.x * f.y by GROUP_6:def 6;
        hence thesis by A30,A32,A34,FUNCT_2:35;
      end;
A35:  (FuncLatt f).a = gr (f.:the carrier of A1) & (FuncLatt f).b = gr (f
      .:the carrier of B1) by A1,A2,Def3;
      consider C1 being strict Subgroup of G1 such that
A36:  C1 = A1 "\/" B1;
A37:  for g1, g2 being Element of G2 st g1 in f.:the carrier of C1 & g2
      in f.:the carrier of C1 holds g1 * g2 in f.:the carrier of C1
      proof
        let g1, g2 be Element of G2;
        assume that
A38:    g1 in f.:the carrier of C1 and
A39:    g2 in f.:the carrier of C1;
        consider x being Element of G1 such that
A40:    x in the carrier of C1 and
A41:    g1 = f.x by A38,FUNCT_2:65;
        consider y being Element of G1 such that
A42:    y in the carrier of C1 and
A43:    g2 = f.y by A39,FUNCT_2:65;
A44:    y in C1 by A42,STRUCT_0:def 5;
        x in C1 by A40,STRUCT_0:def 5;
        then x * y in C1 by A44,GROUP_2:50;
        then
A45:    x * y in the carrier of C1 by STRUCT_0:def 5;
        f.(x * y) = f.x * f.y by GROUP_6:def 6;
        hence thesis by A41,A43,A45,FUNCT_2:35;
      end;
A46:  for g being Element of G2 st g in f.:the carrier of C1 holds g" in
      f.:the carrier of C1
      proof
        let g be Element of G2;
        assume g in f.:the carrier of C1;
        then consider x being Element of G1 such that
A47:    x in the carrier of C1 and
A48:    g = f.x by FUNCT_2:65;
        x in C1 by A47,STRUCT_0:def 5;
        then x" in C1 by GROUP_2:51;
        then
A49:    x" in the carrier of C1 by STRUCT_0:def 5;
        f.x" = (f.x)" by GROUP_6:32;
        hence thesis by A48,A49,FUNCT_2:35;
      end;
      1_G1 in C1 by GROUP_2:46;
      then 1_G1 in the carrier of C1 by STRUCT_0:def 5;
      then f.:the carrier of C1 <> {} by A13,A8,FUNCT_1:def 6;
      then consider C3 being strict Subgroup of G2 such that
A50:  the carrier of C3 = f.:the carrier of C1 by A46,A37,GROUP_2:52;
      ex y being Element of G2 st y = f.1_G1;
      then f.:the carrier of A1 <> {} by A13,A7,FUNCT_1:def 6;
      then consider A3 being strict Subgroup of G2 such that
A51:  the carrier of A3 = f.:the carrier of A1 by A9,A26,GROUP_2:52;
A52:  gr (f.:the carrier of B1) = B3 by A25,Th3;
      the carrier of A3 "\/" B3 = the carrier of C3
      proof
A53:    f.:the carrier of B1 c= the carrier of C3
        proof
          let x be object;
          assume
A54:      x in f.:the carrier of B1;
          then reconsider x as Element of G2;
          consider y being Element of G1 such that
A55:      y in the carrier of B1 and
A56:      x = f.y by A54,FUNCT_2:65;
          y in A by A55,XBOOLE_0:def 3;
          then y in gr A by GROUP_4:29;
          then y in the carrier of gr A by STRUCT_0:def 5;
          then y in the carrier of A1 "\/" B1 by Th4;
          hence thesis by A36,A50,A56,FUNCT_2:35;
        end;
        f.:the carrier of A1 c= the carrier of C3
        proof
          let x be object;
          assume
A57:      x in f.:the carrier of A1;
          then reconsider x as Element of G2;
          consider y being Element of G1 such that
A58:      y in the carrier of A1 and
A59:      x = f.y by A57,FUNCT_2:65;
          y in A by A58,XBOOLE_0:def 3;
          then y in gr A by GROUP_4:29;
          then y in the carrier of gr A by STRUCT_0:def 5;
          then y in the carrier of A1 "\/" B1 by Th4;
          hence thesis by A36,A50,A59,FUNCT_2:35;
        end;
        then B c= the carrier of C3 by A53,XBOOLE_1:8;
        then gr B is Subgroup of C3 by GROUP_4:def 4;
        then the carrier of gr B c= the carrier of C3 by GROUP_2:def 5;
        hence the carrier of A3 "\/" B3 c= the carrier of C3 by A51,A25,Th4;
        reconsider AA = (f"the carrier of A3) \/ f"the carrier of B3 as Subset
        of G1;
A60:    for g being Element of G1 st g in f"the carrier of A3 "\/" B3
        holds g" in f"the carrier of A3 "\/" B3
        proof
          let g be Element of G1;
          assume g in f"the carrier of A3 "\/" B3;
          then f.g in the carrier of A3 "\/" B3 by FUNCT_2:38;
          then f.g in A3 "\/" B3 by STRUCT_0:def 5;
          then (f.g)" in A3 "\/" B3 by GROUP_2:51;
          then f.g" in A3 "\/" B3 by GROUP_6:32;
          then f.g" in the carrier of A3 "\/" B3 by STRUCT_0:def 5;
          hence thesis by FUNCT_2:38;
        end;
        the carrier of B1 c= the carrier of G1 by GROUP_2:def 5;
        then
A61:    the carrier of B1 c= f"the carrier of B3 by A25,FUNCT_2:42;
        the carrier of A1 c= the carrier of G1 by GROUP_2:def 5;
        then the carrier of A1 c= f"the carrier of A3 by A51,FUNCT_2:42;
        then
A62:    A c= AA by A61,XBOOLE_1:13;
A63:    for g1, g2 being Element of G1 st g1 in f"the carrier of A3 "\/"
B3 & g2 in f"the carrier of A3 "\/" B3 holds g1 * g2 in f"the carrier of A3
        "\/" B3
        proof
          let g1, g2 be Element of G1;
          assume that
A64:      g1 in f"the carrier of A3 "\/" B3 and
A65:      g2 in f"the carrier of A3 "\/" B3;
          f.g2 in the carrier of A3 "\/" B3 by A65,FUNCT_2:38;
          then
A66:      f.g2 in A3 "\/" B3 by STRUCT_0:def 5;
          f.g1 in the carrier of A3 "\/" B3 by A64,FUNCT_2:38;
          then f.g1 in A3 "\/" B3 by STRUCT_0:def 5;
          then f.g1 * f.g2 in A3 "\/" B3 by A66,GROUP_2:50;
          then f.(g1 * g2) in A3 "\/" B3 by GROUP_6:def 6;
          then f.(g1 * g2) in the carrier of A3 "\/" B3 by STRUCT_0:def 5;
          hence thesis by FUNCT_2:38;
        end;
A67:    f"the carrier of B3 c= f"the carrier of A3 "\/" B3
        proof
          let x be object;
          assume
A68:      x in f"the carrier of B3;
          then f.x in the carrier of B3 by FUNCT_2:38;
          then
A69:      f.x in B3 by STRUCT_0:def 5;
          f.x in the carrier of G2 by A68,FUNCT_2:5;
          then f.x in A3 "\/" B3 by A69,Th5;
          then f.x in the carrier of A3 "\/" B3 by STRUCT_0:def 5;
          hence thesis by A68,FUNCT_2:38;
        end;
        1_G2 in A3 "\/" B3 by GROUP_2:46;
        then 1_G2 in the carrier of A3 "\/" B3 by STRUCT_0:def 5;
        then f.1_G1 in the carrier of A3 "\/" B3 by GROUP_6:31;
        then f"the carrier of A3 "\/" B3 <> {} by FUNCT_2:38;
        then consider H being strict Subgroup of G1 such that
A70:    the carrier of H = f"the carrier of A3 "\/" B3 by A60,A63,GROUP_2:52;
        f"the carrier of A3 c= f"the carrier of A3 "\/" B3
        proof
          let x be object;
          assume
A71:      x in f"the carrier of A3;
          then f.x in the carrier of A3 by FUNCT_2:38;
          then
A72:      f.x in A3 by STRUCT_0:def 5;
          f.x in the carrier of G2 by A71,FUNCT_2:5;
          then f.x in A3 "\/" B3 by A72,Th5;
          then f.x in the carrier of A3 "\/" B3 by STRUCT_0:def 5;
          hence thesis by A71,FUNCT_2:38;
        end;
        then (f"the carrier of A3) \/ f"the carrier of B3 c= f"the carrier of
        A3 "\/" B3 by A67,XBOOLE_1:8;
        then A c= the carrier of H by A62,A70;
        then gr A is Subgroup of H by GROUP_4:def 4;
        then the carrier of gr A c= the carrier of H by GROUP_2:def 5;
        then
A73:    the carrier of C1 c= f"the carrier of A3 "\/" B3 by A36,A70,Th4;
A74:    f.:the carrier of C1 c= f.:(f"the carrier of A3 "\/" B3)
        proof
          let x be object;
          assume
A75:      x in f.:the carrier of C1;
          then reconsider x as Element of G2;
          ex y being Element of G1 st y in the carrier of C1 & x = f.y by A75,
FUNCT_2:65;
          hence thesis by A73,FUNCT_2:35;
        end;
        f.:f"the carrier of A3 "\/" B3 c= the carrier of A3 "\/" B3 by
FUNCT_1:75;
        hence thesis by A50,A74;
      end;
      then gr (f.:the carrier of A1 "\/" B1) = A3 "\/" B3 by A36,A50,Th3
        .= gr (f.:the carrier of A1) "\/" gr (f.:the carrier of B1) by A51,A52
,Th3
        .= (FuncLatt f).a "\/" (FuncLatt f).b by A35,Th22;
      hence thesis by A1,A2,A24,Th22;
    end;
  end;
  hence thesis by LATTICE4:def 1;
end;

theorem
  for G1, G2 being Group for f being Homomorphism of G1, G2 st f is
  one-to-one holds FuncLatt f is Homomorphism of lattice G1, lattice G2
proof
  let G1, G2 be Group;
  let f be Homomorphism of G1, G2;
  assume f is one-to-one;
  then
A1: FuncLatt f is Semilattice-Homomorphism of lattice G1, lattice G2 by Th31;
  FuncLatt f is sup-Semilattice-Homomorphism of lattice G1, lattice G2 by Th32;
  hence thesis by A1;
end;