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 )
A1: "\/" { (a "/\" b) where b is Element of D : b in X } ,D [= a "/\" ("\/" X,D) by Th32;
A2: a "/\" ("\/" X,D) [= "\/" { (a "/\" b) where b is Element of D : b in X } ,D by Th33;
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;
defpred S₁[ set ] means $1 in X;
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