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;
(L . (((U . X) `) `)) ` = U . ((U . X) `) by ROUGHS_2:def 14, A1;
hence U . ((U . X) `) c= (U . X) ` by A2, A3, SUBSET_1:12; :: thesis: verum