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 U . ((U . X) `) c= (U . X) ` ) holds

for X being Subset of A holds (L . X) ` c= L . ((L . X) `)

let L, U be Function of (bool A),(bool A); :: thesis: ( U = Flip L & ( for X being Subset of A holds U . ((U . X) `) c= (U . X) ` ) implies for X being Subset of A holds (L . X) ` c= L . ((L . X) `) )

assume that

A1: U = Flip L and

A2: for X being Subset of A holds U . ((U . X) `) c= (U . X) ` ; :: thesis: for X being Subset of A holds (L . X) ` c= L . ((L . X) `)

let X be Subset of A; :: thesis: (L . X) ` c= L . ((L . X) `)

((U . (X `)) `) ` c= (U . ((U . (X `)) `)) ` by A2, SUBSET_1:12;

then (L . ((X `) `)) ` c= (U . ((U . (X `)) `)) ` by A1, ROUGHS_2:def 14;

then (L . X) ` c= (U . (((L . X) `) `)) ` by A1, ROUGHS_2:def 14;

then (L . X) ` c= ((L . ((L . X) `)) `) ` by A1, ROUGHS_2:def 14;

hence (L . X) ` c= L . ((L . X) `) ; :: thesis: verum

for X being Subset of A holds (L . X) ` c= L . ((L . X) `)

let L, U be Function of (bool A),(bool A); :: thesis: ( U = Flip L & ( for X being Subset of A holds U . ((U . X) `) c= (U . X) ` ) implies for X being Subset of A holds (L . X) ` c= L . ((L . X) `) )

assume that

A1: U = Flip L and

A2: for X being Subset of A holds U . ((U . X) `) c= (U . X) ` ; :: thesis: for X being Subset of A holds (L . X) ` c= L . ((L . X) `)

let X be Subset of A; :: thesis: (L . X) ` c= L . ((L . X) `)

((U . (X `)) `) ` c= (U . ((U . (X `)) `)) ` by A2, SUBSET_1:12;

then (L . ((X `) `)) ` c= (U . ((U . (X `)) `)) ` by A1, ROUGHS_2:def 14;

then (L . X) ` c= (U . (((L . X) `) `)) ` by A1, ROUGHS_2:def 14;

then (L . X) ` c= ((L . ((L . X) `)) `) ` by A1, ROUGHS_2:def 14;

hence (L . X) ` c= L . ((L . X) `) ; :: thesis: verum