let L be meet-continuous Semilattice; :: thesis: for x being Element of L holds x "/\" is directed-sups-preserving
let x be Element of L; :: thesis: x "/\" is directed-sups-preserving
let X be Subset of L; :: according to WAYBEL_0:def 37 :: thesis: ( X is empty or not X is directed or x "/\" preserves_sup_of X )
assume A1: ( not X is empty & X is directed ) ; :: thesis: x "/\" preserves_sup_of X
reconsider X1 = X as non empty Subset of L by A1;
assume ex_sup_of X,L ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of (x "/\" ) .: X,L & "\/" ((x "/\" ) .: X),L = (x "/\" ) . ("\/" X,L) )
A2: not (x "/\" ) .: X1 is empty ;
(x "/\" ) .: X is directed by A1, YELLOW_2:17;
hence ex_sup_of (x "/\" ) .: X,L by A2, WAYBEL_0:75; :: thesis: "\/" ((x "/\" ) .: X),L = (x "/\" ) . ("\/" X,L)
A3: for x being Element of L
for E being non empty directed Subset of L st x <= sup E holds
x <= sup ({x} "/\" E) by Th45;
thus sup ((x "/\" ) .: X) = "\/" { (x "/\" y) where y is Element of L : y in X } ,L by WAYBEL_1:64
.= sup ({x} "/\" X) by YELLOW_4:42
.= x "/\" (sup X) by A1, A3, Th28
.= (x "/\" ) . (sup X) by WAYBEL_1:def 18 ; :: thesis: verum