theorem Th4: :: TOPGRP_1:4
for H being non empty multMagma
for P, Q, P1, Q1 being Subset of H st P c= P1 & Q c= Q1 holds
P * Q c= P1 * Q1