:: deftheorem defines centered FINSET_1:def 3 :
for F being set holds
( F is centered iff ( F <> {} & ( for G being set st G <> {} & G c= F & G is finite holds
meet G <> {} ) ) );