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

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