theorem Th6: :: FINSET_1:6

for A being set st A is finite holds
for X being Subset-Family of A st X <> {} holds
ex x being set st
( x in X & ( for B being set st B in X & x c= B holds
B = x ) )