theorem :: FINSET_1:12

for F being set st F is finite & F <> {} & F is c=-linear holds
ex m being set st
( m in F & ( for C being set st C in F holds
C c= m ) )