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

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