let G be Group; :: thesis: for H being strict Subgroup of G
for x being Element of G holds
( x in (carr G) . H iff x in H )
let H be strict Subgroup of G; :: thesis: for x being Element of G holds
( x in (carr G) . H iff x in H )
let x be Element of G; :: thesis: ( x in (carr G) . H iff x in H )
thus ( x in (carr G) . H implies x in H ) :: thesis: ( x in H implies x in (carr G) . H )

proof

assume x in (carr G) . H ; :: thesis: x in H
then x in the carrier of H by Def1;
hence x in H by STRUCT_0:def 5; :: thesis: verum

end;

assume A1: x in H ; :: thesis: x in (carr G) . H
(carr G) . H = the carrier of H by Def1;
hence x in (carr G) . H by A1, STRUCT_0:def 5; :: thesis: verum