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)) by Th36;
A2: a "\/" ("/\" (X,D)) [= "/\" ( { (a "\/" b) where b is Element of D : b in X } ,D) by Th35;
hence a "\/" ("/\" (X,D)) = "/\" ( { (a "\/" b) where b is Element of D : b in X } ,D) by A1, LATTICES:8; :: 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;
A3: 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(A3);
hence ("/\" (X,D)) "\/" a = "/\" ( { (b2 "\/" a) where b2 is Element of D : b2 in X } ,D) by A1, A2, LATTICES:8; :: thesis: verum