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