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:15;
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:61
.= sup ({x} "/\" X) by YELLOW_4:42
.= x "/\" (sup X) by A1, A3, Th28
.= (x "/\") . (sup X) by WAYBEL_1:def 18 ; :: thesis: verum