let X be set ; :: thesis: for D being complete /\-distributive Lattice
for a being Element of D holds
( a "\/" ("/\" X,D) = "/\" { (a "\/" b1) where b1 is Element of D : b1 in X } ,D & ("/\" X,D) "\/" a = "/\" { (b2 "\/" a) where b2 is Element of D : b2 in X } ,D )
let D be complete /\-distributive Lattice; :: thesis: for a being Element of D holds
( a "\/" ("/\" X,D) = "/\" { (a "\/" b1) where b1 is Element of D : b1 in X } ,D & ("/\" X,D) "\/" a = "/\" { (b2 "\/" a) where b2 is Element of D : b2 in X } ,D )
let a be Element of D; :: thesis: ( a "\/" ("/\" X,D) = "/\" { (a "\/" b1) where b1 is Element of D : b1 in X } ,D & ("/\" X,D) "\/" a = "/\" { (b2 "\/" a) where b2 is Element of D : b2 in X } ,D )
defpred S₁[ set ] means $1 in X;
A1: ( "/\" { (a "\/" b) where b is Element of D : b in X } ,D [= a "\/" ("/\" X,D) & a "\/" ("/\" X,D) [= "/\" { (a "\/" b) where b is Element of D : b in X } ,D ) by Th35, Th36;
hence a "\/" ("/\" X,D) = "/\" { (a "\/" b) where b is Element of D : b in X } ,D by LATTICES:26; :: thesis: ("/\" X,D) "\/" a = "/\" { (b2 "\/" a) where b2 is Element of D : b2 in X } ,D
deffunc H₄( Element of D) -> Element of the carrier of D = $1 "\/" a;
deffunc H₅( Element of D) -> Element of the carrier of D = a "\/" $1;
A2: for b being Element of D holds H₅(b) = H₄(b) ;
{ H₅(b) where b is Element of D : S₁[b] } = { H₄(c) where c is Element of D : S₁[c] } from FRAENKEL:sch 5(A2);
hence ("/\" X,D) "\/" a = "/\" { (b2 "\/" a) where b2 is Element of D : b2 in X } ,D by A1, LATTICES:26; :: thesis: verum