let C be complete Lattice; ( 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)) )
( ( 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
;
LATTICE3:def 20 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 ;
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;
"/\" ( { (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;
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))
; C is /\-distributive
let X be set ; LATTICE3:def 20 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; ( 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 ) )
; 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; verum