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 )

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 A6; :: thesis: verum

( 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 A6:
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
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)

{ (j . a) where a is Element of L : a in X } is_less_than j . ("\/" X)

j . ("\/" X) [= "\/" ( { (j . a) where a is Element of L : a in X } ,L) by A2;

hence j . ("\/" X) = "\/" ( { (j . a) where a is Element of L : a in X } ,L) by A5, LATTICES:8; :: thesis: verum

end;let X be Subset of L; :: thesis: j . ("\/" X) = "\/" ( { (j . a) where a is Element of L : a in X } ,L)

{ (j . a) where a is Element of L : a in X } is_less_than j . ("\/" X)

proof

then A5:
"\/" ( { (j . a) where a is Element of L : a in X } ,L) [= j . ("\/" X)
by LATTICE3:def 21;
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

A3: x = j . a and

A4: a in X ;

a [= "\/" X by A4, LATTICE3:38;

hence x [= j . ("\/" X) by A1, A3; :: thesis: verum

end;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

A3: x = j . a and

A4: a in X ;

a [= "\/" X by A4, LATTICE3:38;

hence x [= j . ("\/" X) by A1, A3; :: thesis: verum

j . ("\/" X) [= "\/" ( { (j . a) where a is Element of L : a in X } ,L) by A2;

hence j . ("\/" X) = "\/" ( { (j . a) where a is Element of L : a in X } ,L) by A5, LATTICES:8; :: thesis: verum

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 A6; :: thesis: verum