let G be Group; :: thesis: for h being set holds
( h in Subgroups G iff ex H being strict Subgroup of G st h = H )
let h be set ; :: thesis: ( h in Subgroups G iff ex H being strict Subgroup of G st h = H )
thus ( h in Subgroups G implies ex H being strict Subgroup of G st h = H ) :: thesis: ( ex H being strict Subgroup of G st h = H implies h in Subgroups G )

proof

assume h in Subgroups G ; :: thesis: ex H being strict Subgroup of G st h = H
then h is strict Subgroup of G by GROUP_3:def 1;
hence ex H being strict Subgroup of G st h = H ; :: thesis: verum

end;

thus ( ex H being strict Subgroup of G st h = H implies h in Subgroups G ) by GROUP_3:def 1; :: thesis: verum