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 )

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

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 A5:
for X being set
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;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

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