theorem Th24: :: ROUGHS_2:24

for A being non empty set
for L, U being Function of (bool A),(bool A) st U = Flip L & ( for X being Subset of A holds L . (L . X) c= L . X ) holds
for X being Subset of A holds U . X c= U . (U . X)