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