theorem :: WAYBEL_8:30

for X being set
for F being Subset of X holds
( F in the carrier of (CompactSublatt (BoolePoset X)) iff F is finite )