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

end;

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