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

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