let L be complete Lattice; :: thesis: for j being UnOp of L st j is monotone holds
( j is \/-distributive iff for X being Subset of L holds j . ("\/" X) = "\/" { (j . a) where a is Element of L : a in X } ,L )
let j be UnOp of L; :: thesis: ( j is monotone implies ( j is \/-distributive iff for X being Subset of L holds j . ("\/" X) = "\/" { (j . a) where a is Element of L : a in X } ,L ) )
assume A1: j is monotone ; :: thesis: ( j is \/-distributive iff for X being Subset of L holds j . ("\/" X) = "\/" { (j . a) where a is Element of L : a in X } ,L )
thus ( j is \/-distributive implies for X being Subset of L holds j . ("\/" X) = "\/" { (j . a) where a is Element of L : a in X } ,L ) :: thesis: ( ( for X being Subset of L holds j . ("\/" X) = "\/" { (j . a) where a is Element of L : a in X } ,L ) implies j is \/-distributive )

proof

assume A2: for X being Subset of L holds j . ("\/" X) [= "\/" { (j . a) where a is Element of L : a in X } ,L ; :: according to QUANTAL1:def 13 :: thesis: for X being Subset of L holds j . ("\/" X) = "\/" { (j . a) where a is Element of L : a in X } ,L
let X be Subset of L; :: thesis: j . ("\/" X) = "\/" { (j . a) where a is Element of L : a in X } ,L
A3: j . ("\/" X) [= "\/" { (j . a) where a is Element of L : a in X } ,L by A2;
{ (j . a) where a is Element of L : a in X } is_less_than j . ("\/" X)

proof

let x be Element of L; :: according to LATTICE3:def 17 :: thesis: ( not x in { (j . a) where a is Element of L : a in X } or x [= j . ("\/" X) )
assume x in { (j . a) where a is Element of L : a in X } ; :: thesis: x [= j . ("\/" X)
then consider a being Element of L such that
A4: ( x = j . a & a in X ) ;
a [= "\/" X by A4, LATTICE3:38;
hence x [= j . ("\/" X) by A1, A4, Def12; :: thesis: verum

end;

then "\/" { (j . a) where a is Element of L : a in X } ,L [= j . ("\/" X) by LATTICE3:def 21;
hence j . ("\/" X) = "\/" { (j . a) where a is Element of L : a in X } ,L by A3, LATTICES:26; :: thesis: verum

end;

assume A5: for X being Subset of L holds j . ("\/" X) = "\/" { (j . a) where a is Element of L : a in X } ,L ; :: thesis: j is \/-distributive
let X be Subset of L; :: according to QUANTAL1:def 13 :: thesis: j . ("\/" X) [= "\/" { (j . a) where a is Element of L : a in X } ,L
j . ("\/" X) [= j . ("\/" X) ;
hence j . ("\/" X) [= "\/" { (j . a) where a is Element of L : a in X } ,L by A5; :: thesis: verum