let A be non empty set ; :: thesis: 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
let L, U be Function of (bool A),(bool A); :: thesis: ( U = Flip L & ( for X being Subset of A holds L . X c= L . (L . X) ) implies for X being Subset of A holds U . (U . X) c= U . X )
assume that
A1: U = Flip L and
A2: for X being Subset of A holds L . X c= L . (L . X) ; :: thesis: for X being Subset of A holds U . (U . X) c= U . X
let X be Subset of A; :: thesis: U . (U . X) c= U . X
A3: U . X = (L . (X `)) ` by ROUGHS_2:def 14, A1;
U . (U . X) = U . ((L . (X `)) `) by ROUGHS_2:def 14, A1
.= (L . (((L . (X `)) `) `)) ` by ROUGHS_2:def 14, A1
.= (L . (L . (X `))) ` ;
hence U . (U . X) c= U . X by A3, A2, SUBSET_1:12; :: thesis: verum