theorem Conv4: :: ROUGHS_3:32

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) `)