let L be non empty reflexive antisymmetric RelStr ; :: thesis: ( ( for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) ) implies L is satisfying_MC )
assume A1: for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) ; :: thesis: L is satisfying_MC
let x be Element of L; :: according to WAYBEL_2:def 6 :: thesis: for D being non empty directed Subset of L holds x "/\" (sup D) = sup ({x} "/\" D)
let D be non empty directed Subset of L; :: thesis: x "/\" (sup D) = sup ({x} "/\" D)
A2: {x} is directed by WAYBEL_0:5;
thus x "/\" (sup D) = (sup {x}) "/\" (sup D) by YELLOW_0:39
.= sup ({x} "/\" D) by A1, A2 ; :: thesis: verum