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