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 "/\" a') where a' is Element of C : a' in X } is_less_than c & ( for d being Element of C st { (b "/\" b') where b' is Element of C : b' 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 } ;
( X is_less_than "\/" X,C & ( for d being Element of C st X is_less_than d holds
"\/" X,C [= d ) & { (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 & ( 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; :: thesis: verum

end;

assume A2: 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 "/\" a') where a' is Element of C : a' in X } is_less_than c & ( for d being Element of C st { (b "/\" a') where a' is Element of C : a' 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 "/\" a') where a' is Element of C : a' in X } is_less_than c & ( for d being Element of C st { (b "/\" a') where a' is Element of C : a' in X } is_less_than d holds
c [= d ) implies b "/\" a [= c )
assume ( X is_less_than a & ( for d being Element of C st X is_less_than d holds
a [= d ) & { (b "/\" a') where a' is Element of C : a' in X } is_less_than c & ( for d being Element of C st { (b "/\" b') where b' is Element of C : b' in X } is_less_than d holds
c [= d ) ) ; :: thesis: b "/\" a [= c
then ( a = "\/" X,C & c = "\/" { (b "/\" a') where a' is Element of C : a' in X } ,C ) by Def21;
hence b "/\" a [= c by A2; :: thesis: verum