theorem :: SETFAM_1:5

for X, Z being set st X <> {} & ( for Z1 being set st Z1 in X holds
Z c= Z1 ) holds
Z c= meet X