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 ;

per cases ( x in N ` A or x in N ` B ) by A1, XBOOLE_0:def 3;

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

then x * N c= A \/ B by Th12, XBOOLE_1:10;
hence x in N ` (A \/ B) ; :: thesis: verum

end;

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

then x * N c= A \/ B by Th12, XBOOLE_1:10;
hence x in N ` (A \/ B) ; :: thesis: verum

end;

end;