theorem Th15: :: GLIBPRE0:14

for X being non empty set st ( for a being set st a in X holds
a is cardinal number ) holds
ex A being Cardinal st
( A in X & A = meet X )