theorem Th6: :: WAYBEL22:6

for L being non empty upper-bounded with_infima Poset holds InclPoset (Filt L) is CLSubFrame of BoolePoset the carrier of L