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

proof

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

end;

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