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

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