let G be Group; :: thesis: for p being Element of (lattice G)
for H being Subgroup of G st p = H holds
H is strict Subgroup of G
let p be Element of (lattice G); :: thesis: for H being Subgroup of G st p = H holds
H is strict Subgroup of G
let H be Subgroup of G; :: thesis: ( p = H implies H is strict Subgroup of G )
assume A1: p = H ; :: thesis: H is strict Subgroup of G
the carrier of (lattice G) = Subgroups G ;
reconsider h = p as strict Subgroup of G by GROUP_3:def 1;
h = H by A1;
hence H is strict Subgroup of G ; :: thesis: verum