let H be non empty multMagma ; :: thesis: for P, Q, P1, Q1 being Subset of H st P c= P1 & Q c= Q1 holds
P * Q c= P1 * Q1
let P, Q, P1, Q1 be Subset of H; :: thesis: ( P c= P1 & Q c= Q1 implies P * Q c= P1 * Q1 )
assume A1: ( P c= P1 & Q c= Q1 ) ; :: thesis: P * Q c= P1 * Q1
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P * Q or x in P1 * Q1 )
assume x in P * Q ; :: thesis: x in P1 * Q1
then ex g, t being Element of H st
( x = g * t & g in P & t in Q ) ;
hence x in P1 * Q1 by A1; :: thesis: verum