let C be complete Lattice; :: thesis: ( C is \/-distributive iff for X being set
for a being Element of C holds a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) )
thus ( C is \/-distributive implies for X being set
for a being Element of C holds a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) ) :: thesis: ( ( for X being set
for a being Element of C holds a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) ) implies C is \/-distributive )

proof

assume A1: for X being set
for a, b, c being Element of C st X is_less_than a & ( for d being Element of C st X is_less_than d holds
a [= d ) & { (b "/\" a9) where a9 is Element of C : a9 in X } is_less_than c & ( for d being Element of C st { (b "/\" b9) where b9 is Element of C : b9 in X } is_less_than d holds
c [= d ) holds
b "/\" a [= c ; :: according to LATTICE3:def 19 :: thesis: for X being set
for a being Element of C holds a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C)
let X be set ; :: thesis: for a being Element of C holds a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C)
let a be Element of C; :: thesis: a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C)
set Y = { (a "/\" b) where b is Element of C : b in X } ;
A2: X is_less_than "\/" (X,C) by Def21;
A3: for d being Element of C st X is_less_than d holds
"\/" (X,C) [= d by Def21;
A4: { (a "/\" b) where b is Element of C : b in X } is_less_than "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) by Def21;
for d being Element of C st { (a "/\" b) where b is Element of C : b in X } is_less_than d holds
"\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) [= d by Def21;
hence a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) by A1, A2, A3, A4; :: thesis: verum

end;

assume A5: for X being set
for a being Element of C holds a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) ; :: thesis: C is \/-distributive
let X be set ; :: according to LATTICE3:def 19 :: thesis: for a, b, c being Element of C st X is_less_than a & ( for d being Element of C st X is_less_than d holds
a [= d ) & { (b "/\" a9) where a9 is Element of C : a9 in X } is_less_than c & ( for d being Element of C st { (b "/\" a9) where a9 is Element of C : a9 in X } is_less_than d holds
c [= d ) holds
b "/\" a [= c
let a, b, c be Element of C; :: thesis: ( X is_less_than a & ( for d being Element of C st X is_less_than d holds
a [= d ) & { (b "/\" a9) where a9 is Element of C : a9 in X } is_less_than c & ( for d being Element of C st { (b "/\" a9) where a9 is Element of C : a9 in X } is_less_than d holds
c [= d ) implies b "/\" a [= c )
assume A6: ( X is_less_than a & ( for d being Element of C st X is_less_than d holds
a [= d ) & { (b "/\" a9) where a9 is Element of C : a9 in X } is_less_than c & ( for d being Element of C st { (b "/\" b9) where b9 is Element of C : b9 in X } is_less_than d holds
c [= d ) ) ; :: thesis: b "/\" a [= c
then A7: a = "\/" (X,C) by Def21;
c = "\/" ( { (b "/\" a9) where a9 is Element of C : a9 in X } ,C) by A6, Def21;
hence b "/\" a [= c by A5, A7; :: thesis: verum