theorem Th43: :: WAYBEL_0:43

for L being with_infima Poset
for X being non empty upper Subset of L holds
( X is filtered iff for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in X )