let G be Group; :: thesis: Bottom (lattice G) = (1). G
set L = lattice G;
reconsider E = (1). G as Element of (lattice G) by GROUP_3:def 1;

now :: thesis: for A being Element of (lattice G) holds A "/\" E = E

let A be Element of (lattice G); :: thesis: A "/\" E = E
reconsider H = A as strict Subgroup of G by GROUP_3:def 1;
thus A "/\" E = (SubMeet G) . (A,E) by LATTICES:def 2
.= H /\ ((1). G) by Def11
.= E by GROUP_2:85 ; :: thesis: verum

end;

hence Bottom (lattice G) = (1). G by RLSUB_2:64; :: thesis: verum