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

for N being Subgroup of G holds (N ` A) \/ (N ` B) c= N ` (A \/ B)

let A, B be non empty Subset of G; :: thesis: for N being Subgroup of G holds (N ` A) \/ (N ` B) c= N ` (A \/ B)

let N be Subgroup of G; :: thesis: (N ` A) \/ (N ` B) c= N ` (A \/ B)

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

assume A1: x in (N ` A) \/ (N ` B) ; :: thesis: x in N ` (A \/ B)

then reconsider x = x as Element of G ;

for N being Subgroup of G holds (N ` A) \/ (N ` B) c= N ` (A \/ B)

let A, B be non empty Subset of G; :: thesis: for N being Subgroup of G holds (N ` A) \/ (N ` B) c= N ` (A \/ B)

let N be Subgroup of G; :: thesis: (N ` A) \/ (N ` B) c= N ` (A \/ B)

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

assume A1: x in (N ` A) \/ (N ` B) ; :: thesis: x in N ` (A \/ B)

then reconsider x = x as Element of G ;