let H be distributive complete LATTICE; :: thesis: for a being Element of H
for X being finite Subset of H holds a "/\" preserves_sup_of X
let a be Element of H; :: thesis: for X being finite Subset of H holds a "/\" preserves_sup_of X
let X be finite Subset of H; :: thesis: a "/\" preserves_sup_of X
assume ex_sup_of X,H ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of (a "/\" ) .: X,H & "\/" ((a "/\" ) .: X),H = (a "/\" ) . ("\/" X,H) )
thus ex_sup_of (a "/\" ) .: X,H by YELLOW_0:17; :: thesis: "\/" ((a "/\" ) .: X),H = (a "/\" ) . ("\/" X,H)
thus sup ((a "/\" ) .: X) = "\/" { (a "/\" y) where y is Element of H : y in X } ,H by WAYBEL_1:64
.= sup ({a} "/\" X) by YELLOW_4:42
.= a "/\" (sup X) by Th15
.= (a "/\" ) . (sup X) by WAYBEL_1:def 18 ; :: thesis: verum