let G be Group; :: thesis: for g being Element of G
for H being Subgroup of G st g in H holds
g " in H
let g be Element of G; :: thesis: for H being Subgroup of G st g in H holds
g " in H
let H be Subgroup of G; :: thesis: ( g in H implies g " in H )
assume g in H ; :: thesis: g " in H
then reconsider h = g as Element of H by STRUCT_0:def 5;
h " in H by STRUCT_0:def 5;
hence g " in H by Th57; :: thesis: verum