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