let L be meet-continuous Semilattice; for x being Element of L holds x "/\" is directed-sups-preserving
let x be Element of L; x "/\" is directed-sups-preserving
let X be Subset of L; WAYBEL_0:def 37 ( X is empty or not X is directed or x "/\" preserves_sup_of X )
assume A1:
( not X is empty & X is directed )
; x "/\" preserves_sup_of X
reconsider X1 = X as non empty Subset of L by A1;
assume
ex_sup_of X,L
; WAYBEL_0:def 31 ( 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; "\/" (((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
; verum