let G be Group; :: thesis:
let Y be Subset of (lattice G); :: according to VECTSP_8:def 6 :: thesis:

per cases ;

suppose A1: Y = {} ; :: thesis:

take Top (lattice G) ; :: thesis:
thus Top (lattice G) is_less_than Y by A1; :: thesis:
let b be Element of (lattice G); :: thesis:
assume b is_less_than Y ; :: thesis:
thus b [= Top (lattice G) by LATTICES:19; :: thesis:

end;

suppose Y <> {} ; :: thesis:

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 ; :: thesis:
set x = the Element of X;
thus p is_less_than Y :: thesis:

proof

let q be Element of (lattice G); :: according to LATTICE3:def 16 :: thesis:
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 ; :: thesis:
(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 p [= q by Th25; :: thesis:

end;

let r be Element of (lattice G); :: thesis:
reconsider H = r as Subgroup of G by GROUP_3:def 1;
assume A3: r is_less_than Y ; :: thesis:
A4: for Z1 being set st Z1 in (carr G) .: X holds
the carrier of H c= Z1

proof

let Z1 be set ; :: thesis:
assume A5: Z1 in (carr G) .: X ; :: thesis:
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 = 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 the carrier of H c= Z1 by Th25; :: thesis:

end;

(carr G) . the Element of 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 r [= p by Th25; :: thesis:

end;

end;