let Q be Quantale; :: thesis: for j being UnOp of Q st j is monotone & j is idempotent & j is \/-distributive holds
ex L being complete Lattice st
( the carrier of L = rng j & ( for X being Subset of holds "\/" X = j . ("\/" X,Q) ) )
let j be UnOp of Q; :: thesis: ( j is monotone & j is idempotent & j is \/-distributive implies ex L being complete Lattice st
( the carrier of L = rng j & ( for X being Subset of holds "\/" X = j . ("\/" X,Q) ) ) )
assume A1: ( j is monotone & j is idempotent & j is \/-distributive ) ; :: thesis: ex L being complete Lattice st
( the carrier of L = rng j & ( for X being Subset of holds "\/" X = j . ("\/" X,Q) ) )
reconsider D = rng j as non empty Subset of ;
dom j = H₁(Q) by FUNCT_2:def 1;
then reconsider j' = j as Function of H₁(Q),D by RELSET_1:11;
deffunc H₅( Subset of ) -> Element of D = j' . ("\/" $1,Q);
consider f being Function of bool D,D such that
A2: for X being Subset of holds f . X = H₅(X) from FUNCT_2:sch 4();
A3: dom f = bool D by FUNCT_2:def 1;
A4: for X being Subset-Family of holds f . (f .: X) = f . (union X)

proof

let X be Subset-Family of ; :: thesis: f . (f .: X) = f . (union X)
set A = { (j . a) where a is Element of : a in f .: X } ;
set B = { (j . b) where b is Element of : b in union X } ;
reconsider Y = f .: X, X' = union X as Subset of by XBOOLE_1:1;

now

let a be Element of ; :: thesis: ( a in { (j . b) where b is Element of : b in union X } implies ex b being Element of the carrier of Q st
( a [= b & b in { (j . a) where a is Element of : a in f .: X } ) )
assume a in { (j . b) where b is Element of : b in union X } ; :: thesis: ex b being Element of the carrier of Q st
( a [= b & b in { (j . a) where a is Element of : a in f .: X } )
then consider b' being Element of such that
A5: a = j . b' and
A6: b' in union X ;
consider Y being set such that
A7: b' in Y and
A8: Y in X by A6, TARSKI:def 4;
reconsider Y = Y as Subset of by A8;
A9: b' [= "\/" Y,Q by A7, LATTICE3:38;
take b = j . ("\/" Y,Q); :: thesis: ( a [= b & b in { (j . a) where a is Element of : a in f .: X } )
b = f . Y by A2;
then A10: b in f .: X by A3, A8, FUNCT_1:def 12;
j . b = b by A1, Lm1;
hence ( a [= b & b in { (j . a) where a is Element of : a in f .: X } ) by A1, A5, A10, A9, Def12; :: thesis: verum

end;

then A11: "\/" { (j . b) where b is Element of : b in union X } ,Q [= "\/" { (j . a) where a is Element of : a in f .: X } ,Q by LATTICE3:48;
{ (j . a) where a is Element of : a in f .: X } is_less_than "\/" { (j . b) where b is Element of : b in union X } ,Q

proof

let a be Element of ; :: according to LATTICE3:def 17 :: thesis: ( not a in { (j . a) where a is Element of : a in f .: X } or a [= "\/" { (j . b) where b is Element of : b in union X } ,Q )
assume a in { (j . a) where a is Element of : a in f .: X } ; :: thesis: a [= "\/" { (j . b) where b is Element of : b in union X } ,Q
then consider a' being Element of such that
A12: a = j . a' and
A13: a' in f .: X ;
consider x being set such that
A14: x in dom f and
A15: x in X and
A16: a' = f . x by A13, FUNCT_1:def 12;
reconsider x = x as Subset of by A14;
reconsider Y = x as Subset of by XBOOLE_1:1;
A17: { (j . b) where b is Element of : b in Y } c= { (j . b) where b is Element of : b in union X }

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in { (j . b) where b is Element of : b in Y } or z in { (j . b) where b is Element of : b in union X } )
assume z in { (j . b) where b is Element of : b in Y } ; :: thesis: z in { (j . b) where b is Element of : b in union X }
then consider b being Element of such that
A18: z = j . b and
A19: b in Y ;
b in union X by A15, A19, TARSKI:def 4;
hence z in { (j . b) where b is Element of : b in union X } by A18; :: thesis: verum

end;

a' = j . ("\/" Y) by A2, A16;
then a' = "\/" { (j . b) where b is Element of : b in Y } ,Q by A1, Th10;
then a' [= "\/" { (j . b) where b is Element of : b in union X } ,Q by A17, LATTICE3:46;
then a [= j . ("\/" { (j . b) where b is Element of : b in union X } ,Q) by A1, A12, Def12;
then a [= j . (j . ("\/" X')) by A1, Th10;
then a [= j . ("\/" X') by A1, Lm1;
hence a [= "\/" { (j . b) where b is Element of : b in union X } ,Q by A1, Th10; :: thesis: verum

end;

then A20: "\/" { (j . a) where a is Element of : a in f .: X } ,Q [= "\/" { (j . b) where b is Element of : b in union X } ,Q by LATTICE3:def 21;
thus f . (f .: X) = j . ("\/" Y) by A2
.= "\/" { (j . a) where a is Element of : a in f .: X } ,Q by A1, Th10
.= "\/" { (j . b) where b is Element of : b in union X } ,Q by A20, A11, LATTICES:26
.= j . ("\/" X') by A1, Th10
.= f . (union X) by A2 ; :: thesis: verum

end;

for a being Element of D holds f . {a} = a

proof

let a be Element of D; :: thesis: f . {a} = a
consider a' being set such that
A21: a' in dom j and
A22: a = j . a' by FUNCT_1:def 5;
reconsider x = a as Element of ;
reconsider x' = {x} as Subset of ;
reconsider a' = a' as Element of by A21;
thus f . {a} = j . ("\/" x') by A2
.= j . (j . a') by A22, LATTICE3:43
.= a by A1, A22, Lm1 ; :: thesis: verum

end;

then consider L being strict complete Lattice such that
A23: H₁(L) = D and
A24: for X being Subset of holds "\/" X = f . X by A4, LATTICE3:56;
take L ; :: thesis: ( the carrier of L = rng j & ( for X being Subset of holds "\/" X = j . ("\/" X,Q) ) )
thus H₁(L) = rng j by A23; :: thesis: for X being Subset of holds "\/" X = j . ("\/" X,Q)
let X be Subset of ; :: thesis: "\/" X = j . ("\/" X,Q)
thus "\/" X = f . X by A24
.= j . ("\/" X,Q) by A2, A23 ; :: thesis: verum
consider q being Element of ;