theorem Th26: :: WAYBEL12:26

for L being with_infima Poset
for X being Subset of L st X is Open & X is lower holds
X is filtered