for X1 being non empty set st ( for x1 being Element of X1 st P₁[x1] holds
P₂[x1] ) holds
{ y1 where y1 is Element of X1 : P₁[y1] } c= { z1 where z1 is Element of X1 : P₂[z1] }