for X being set
for SFX being Subset-Family of X holds
( ( SFX is cap-closed & X in SFX ) iff FinMeetCl SFX c= SFX )