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:61
.= sup ({a} "/\" X) by YELLOW_4:42
.= a "/\" (sup X) by Th15
.= (a "/\") . (sup X) by WAYBEL_1:def 18 ; :: thesis: verum