theorem Th3: :: SETFAM_1:3

for X, Z being set st Z in X holds
meet X c= Z by Def1;