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

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