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) ) )
consider q being Element of Q;
A2: ( dom j = H₁(Q) & rng j c= H₁(Q) & q in H₁(Q) ) by FUNCT_2:def 1;
reconsider D = rng j as non empty Subset of Q ;
reconsider j' = j as Function of H₁(Q),D by A2, RELSET_1:11;
deffunc H₅( Subset of D) -> Element of D = j' . ("\/" $1,Q);
consider f being Function of (bool D),D such that
A3: for X being Subset of D holds f . X = H₅(X) from FUNCT_2:sch 4();
A4: dom f = bool D by FUNCT_2:def 1;
A5: 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
A6: ( a' in dom j & a = j . a' ) by FUNCT_1:def 5;
reconsider a' = a' as Element of Q by A6;
reconsider x = a as Element of Q ;
reconsider x' = {x} as Subset of Q ;
thus f . {a} = j . ("\/" x') by A3
.= j . (j . a') by A6, LATTICE3:43
.= a by A1, A6, Lm1 ; :: thesis: verum

end;

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, X' = union X as Subset of Q by XBOOLE_1:1;
{ (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 a' being Element of Q such that
A7: ( a = j . a' & a' in f .: X ) ;
consider x being set such that
A8: ( x in dom f & x in X & a' = f . x ) by A7, FUNCT_1:def 12;
reconsider x = x as Subset of D by A8;
reconsider Y = x as Subset of Q by XBOOLE_1:1;
a' = j . ("\/" Y) by A3, A8;
then A9: a' = "\/" { (j . b) where b is Element of Q : b in Y } ,Q by A1, Th10;
{ (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 set ; :: 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
A10: ( z = j . b & b in Y ) ;
b in union X by A8, A10, TARSKI:def 4;
hence z in { (j . b) where b is Element of Q : b in union X } by A10; :: thesis: verum

end;

then a' [= "\/" { (j . b) where b is Element of Q : b in union X } ,Q by A9, LATTICE3:46;
then a [= j . ("\/" { (j . b) where b is Element of Q : b in union X } ,Q) by A1, A7, 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 Q : b in union X } ,Q by A1, Th10; :: thesis: verum

end;

then A11: "\/" { (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;

now

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 b' being Element of Q such that
A12: ( a = j . b' & b' in union X ) ;
consider Y being set such that
A13: ( b' in Y & Y in X ) by A12, TARSKI:def 4;
reconsider Y = Y as Subset of D by A13;
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 A3;
then ( b in f .: X & j . b = b & b' [= "\/" Y,Q ) by A1, A4, A13, Lm1, FUNCT_1:def 12, LATTICE3:38;
hence ( a [= b & b in { (j . a) where a is Element of Q : a in f .: X } ) by A1, A12, Def12; :: thesis: verum

end;

then A14: "\/" { (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:48;
thus f . (f .: X) = j . ("\/" Y) by A3
.= "\/" { (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 A11, A14, LATTICES:26
.= j . ("\/" X') by A1, Th10
.= f . (union X) by A3 ; :: thesis: verum

end;

then consider L being strict complete Lattice such that
A15: ( H₁(L) = D & ( for X being Subset of L holds "\/" X = f . X ) ) by A5, LATTICE3:56;
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 A15; :: 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 A15
.= j . ("\/" X,Q) by A3, A15 ; :: thesis: verum