theorem :: SETFAM_1:7

for X, Y, Z being set st X in Y & X c= Z holds
meet Y c= Z