theorem :: GLIBPRE0:15

for X being set st ( for a being set st a in X holds
a is cardinal number ) holds
meet X is cardinal number