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