theorem R224: :: ROUGHS_3:6

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 . X c= L . (L . X) ) holds
for X being Subset of A holds U . (U . X) c= U . X