let G be Group; :: thesis: for A being non empty Subset of G

for N, H being Subgroup of G st N is Subgroup of H holds

N ~ A c= H ~ A

let A be non empty Subset of G; :: thesis: for N, H being Subgroup of G st N is Subgroup of H holds

N ~ A c= H ~ A

let N, H be Subgroup of G; :: thesis: ( N is Subgroup of H implies N ~ A c= H ~ A )

assume A1: N is Subgroup of H ; :: thesis: N ~ A c= H ~ A

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in N ~ A or x in H ~ A )

assume A2: x in N ~ A ; :: thesis: x in H ~ A

then reconsider x = x as Element of G ;

x * N meets A by A2, Th14;

then x * H meets A by A1, GROUP_3:6, XBOOLE_1:63;

hence x in H ~ A ; :: thesis: verum

for N, H being Subgroup of G st N is Subgroup of H holds

N ~ A c= H ~ A

let A be non empty Subset of G; :: thesis: for N, H being Subgroup of G st N is Subgroup of H holds

N ~ A c= H ~ A

let N, H be Subgroup of G; :: thesis: ( N is Subgroup of H implies N ~ A c= H ~ A )

assume A1: N is Subgroup of H ; :: thesis: N ~ A c= H ~ A

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in N ~ A or x in H ~ A )

assume A2: x in N ~ A ; :: thesis: x in H ~ A

then reconsider x = x as Element of G ;

x * N meets A by A2, Th14;

then x * H meets A by A1, GROUP_3:6, XBOOLE_1:63;

hence x in H ~ A ; :: thesis: verum