let L be with_suprema Poset; :: thesis: ( ( for X being directed Subset of L

for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" X) ) implies for X being Subset of L

for x being Element of L st ex_sup_of X,L holds

x "/\" (sup X) = sup ({x} "/\" (finsups X)) )

assume A1: for X being directed Subset of L

for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" X) ; :: thesis: for X being Subset of L

for x being Element of L st ex_sup_of X,L holds

x "/\" (sup X) = sup ({x} "/\" (finsups X))

let X be Subset of L; :: thesis: for x being Element of L st ex_sup_of X,L holds

x "/\" (sup X) = sup ({x} "/\" (finsups X))

let x be Element of L; :: thesis: ( ex_sup_of X,L implies x "/\" (sup X) = sup ({x} "/\" (finsups X)) )

assume ex_sup_of X,L ; :: thesis: x "/\" (sup X) = sup ({x} "/\" (finsups X))

hence x "/\" (sup X) = x "/\" (sup (finsups X)) by WAYBEL_0:55

.= sup ({x} "/\" (finsups X)) by A1 ;

:: thesis: verum

for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" X) ) implies for X being Subset of L

for x being Element of L st ex_sup_of X,L holds

x "/\" (sup X) = sup ({x} "/\" (finsups X)) )

assume A1: for X being directed Subset of L

for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" X) ; :: thesis: for X being Subset of L

for x being Element of L st ex_sup_of X,L holds

x "/\" (sup X) = sup ({x} "/\" (finsups X))

let X be Subset of L; :: thesis: for x being Element of L st ex_sup_of X,L holds

x "/\" (sup X) = sup ({x} "/\" (finsups X))

let x be Element of L; :: thesis: ( ex_sup_of X,L implies x "/\" (sup X) = sup ({x} "/\" (finsups X)) )

assume ex_sup_of X,L ; :: thesis: x "/\" (sup X) = sup ({x} "/\" (finsups X))

hence x "/\" (sup X) = x "/\" (sup (finsups X)) by WAYBEL_0:55

.= sup ({x} "/\" (finsups X)) by A1 ;

:: thesis: verum