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