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