let G be Group; :: thesis: Top (lattice G) = (Omega). G
set L = lattice G;
reconsider E = (Omega). 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 = (SubJoin G) . (A,E) by LATTICES:def 1
.= H "\/" ((Omega). G) by Def10
.= E by Th59 ; :: thesis: verum
end;
hence Top (lattice G) = (Omega). G by RLSUB_2:65; :: thesis: verum