let x be object ; :: thesis: for G being addGroup
for a being Element of G
for H being Subgroup of G holds
( x in a + H iff ex g being Element of G st
( x = a + g & g in H ) )
let G be addGroup; :: thesis: for a being Element of G
for H being Subgroup of G holds
( x in a + H iff ex g being Element of G st
( x = a + g & g in H ) )
let a be Element of G; :: thesis: for H being Subgroup of G holds
( x in a + H iff ex g being Element of G st
( x = a + g & g in H ) )
let H be Subgroup of G; :: thesis: ( x in a + H iff ex g being Element of G st
( x = a + g & g in H ) )
thus ( x in a + H implies ex g being Element of G st
( x = a + g & g in H ) ) :: thesis: ( ex g being Element of G st
( x = a + g & g in H ) implies x in a + H )

proof

assume x in a + H ; :: thesis: ex g being Element of G st
( x = a + g & g in H )
then consider g being Element of G such that
A1: ( x = a + g & g in carr H ) by Th27;
take g ; :: thesis: ( x = a + g & g in H )
thus ( x = a + g & g in H ) by A1; :: thesis: verum

end;

given g being Element of G such that A2: x = a + g and
A3: g in H ; :: thesis: x in a + H
thus x in a + H by A2, A3, Th27; :: thesis: verum