let L be non empty reflexive antisymmetric with_infima satisfying_MC RelStr ; :: thesis: for x being Element of L
for D being non empty directed Subset of L st x <= sup D holds
x = sup ({x} "/\" D)
let x be Element of L; :: thesis: for D being non empty directed Subset of L st x <= sup D holds
x = sup ({x} "/\" D)
let D be non empty directed Subset of L; :: thesis: ( x <= sup D implies x = sup ({x} "/\" D) )
assume x <= sup D ; :: thesis: x = sup ({x} "/\" D)
hence x = x "/\" (sup D) by YELLOW_0:25
.= sup ({x} "/\" D) by Def6 ;
:: thesis: verum