theorem :: FINSET_1:11

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
m c= C ) )