for X being non empty set
for SFX being Subset-Family of X holds
( SFX is non empty with_non-empty_elements cap-closed upper Subset-Family of X iff SFX is Filter of X ) by Lm01, Lm02;