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

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