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: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;
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:26; :: thesis: verum