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

for N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds

N ~ A c= (N1 ~ A) /\ (N2 ~ A)

let A be non empty Subset of G; :: thesis: for N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds

N ~ A c= (N1 ~ A) /\ (N2 ~ A)

let N, N1, N2 be Subgroup of G; :: thesis: ( N = N1 /\ N2 implies N ~ A c= (N1 ~ A) /\ (N2 ~ A) )

assume N = N1 /\ N2 ; :: thesis: N ~ A c= (N1 ~ A) /\ (N2 ~ A)

then A1: ( N is Subgroup of N1 & N is Subgroup of N2 ) by GROUP_2:88;

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

assume A2: x in N ~ A ; :: thesis: x in (N1 ~ A) /\ (N2 ~ A)

( N ~ A c= N1 ~ A & N ~ A c= N2 ~ A ) by A1, Th26;

hence x in (N1 ~ A) /\ (N2 ~ A) by A2, XBOOLE_0:def 4; :: thesis: verum

for N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds

N ~ A c= (N1 ~ A) /\ (N2 ~ A)

let A be non empty Subset of G; :: thesis: for N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds

N ~ A c= (N1 ~ A) /\ (N2 ~ A)

let N, N1, N2 be Subgroup of G; :: thesis: ( N = N1 /\ N2 implies N ~ A c= (N1 ~ A) /\ (N2 ~ A) )

assume N = N1 /\ N2 ; :: thesis: N ~ A c= (N1 ~ A) /\ (N2 ~ A)

then A1: ( N is Subgroup of N1 & N is Subgroup of N2 ) by GROUP_2:88;

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

assume A2: x in N ~ A ; :: thesis: x in (N1 ~ A) /\ (N2 ~ A)

( N ~ A c= N1 ~ A & N ~ A c= N2 ~ A ) by A1, Th26;

hence x in (N1 ~ A) /\ (N2 ~ A) by A2, XBOOLE_0:def 4; :: thesis: verum