theorem Th13: :: WAYBEL15:13

for X being set
for c being Function of (BoolePoset X),(BoolePoset X) st c is idempotent & c is directed-sups-preserving holds
inclusion c is directed-sups-preserving