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 L 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 L 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 L holds "\/" X = j . ("\/" (X,Q)) ) )
reconsider D = rng j as non empty Subset of Q ;
dom j = H₁(Q) by FUNCT_2:def 1;
then reconsider j9 = j as Function of H₁(Q),D by RELSET_1:4;
deffunc H₅( Subset of D) -> Element of D = j9 . ("\/" ($1,Q));
consider f being Function of (bool D),D such that
A2: for X being Subset of D 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 D holds f . (f .: X) = f . (union X)

proof

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

now :: thesis: for a being Element of Q st a in { (j . b) where b is Element of Q : b in union X } holds
ex b being Element of the carrier of Q st
( a [= b & b in { (j . a) where a is Element of Q : a in f .: X } )

let a be Element of Q; :: thesis: ( a in { (j . b) where b is Element of Q : 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 Q : a in f .: X } ) )
assume a in { (j . b) where b is Element of Q : 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 Q : a in f .: X } )
then consider b9 being Element of Q such that
A5: a = j . b9 and
A6: b9 in union X ;
consider Y being set such that
A7: b9 in Y and
A8: Y in X by A6, TARSKI:def 4;
reconsider Y = Y as Subset of D by A8;
A9: b9 [= "\/" (Y,Q) by A7, LATTICE3:38;
take b = j . ("\/" (Y,Q)); :: thesis: ( a [= b & b in { (j . a) where a is Element of Q : a in f .: X } )
b = f . Y by A2;
then A10: b in f .: X by A3, A8, FUNCT_1:def 6;
j . b = b by A1, Lm1;
hence ( a [= b & b in { (j . a) where a is Element of Q : a in f .: X } ) by A1, A5, A10, A9; :: thesis: verum

end;

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

proof

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

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { (j . b) where b is Element of Q : b in Y } or z in { (j . b) where b is Element of Q : b in union X } )
assume z in { (j . b) where b is Element of Q : b in Y } ; :: thesis: z in { (j . b) where b is Element of Q : b in union X }
then consider b being Element of Q 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 Q : b in union X } by A18; :: thesis: verum

end;

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

end;

then A20: "\/" ( { (j . a) where a is Element of Q : a in f .: X } ,Q) [= "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q) by LATTICE3:def 21;
thus f . (f .: X) = j . ("\/" Y) by A2
.= "\/" ( { (j . a) where a is Element of Q : a in f .: X } ,Q) by A1, Th10
.= "\/" ( { (j . b) where b is Element of Q : b in union X } ,Q) by A20, A11, LATTICES:8
.= j . ("\/" X9) 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 a9 being object such that
A21: a9 in dom j and
A22: a = j . a9 by FUNCT_1:def 3;
reconsider x = a as Element of Q ;
reconsider x9 = {x} as Subset of Q ;
reconsider a9 = a9 as Element of Q by A21;
thus f . {a} = j . ("\/" x9) by A2
.= j . (j . a9) by A22, LATTICE3:42
.= 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 L holds "\/" X = f . X by A4, LATTICE3:55;
take L ; :: thesis: ( the carrier of L = rng j & ( for X being Subset of L holds "\/" X = j . ("\/" (X,Q)) ) )
thus H₁(L) = rng j by A23; :: thesis: for X being Subset of L holds "\/" X = j . ("\/" (X,Q))
let X be Subset of L; :: thesis: "\/" X = j . ("\/" (X,Q))
thus "\/" X = f . X by A24
.= j . ("\/" (X,Q)) by A2, A23 ; :: thesis: verum