let S be non empty reflexive RelStr ; :: thesis: ( ( for X being Subset of
for x being Element of holds x "/\" (sup X) = "\/" { (x "/\" y) where y is Element of : y in X } ,S ) implies S is satisfying_MC )
assume A1: for X being Subset of
for x being Element of holds x "/\" (sup X) = "\/" { (x "/\" y) where y is Element of : y in X } ,S ; :: thesis: S is satisfying_MC
let y be Element of ; :: according to WAYBEL_2:def 6 :: thesis: for D being non empty directed Subset of holds y "/\" (sup D) = sup ({y} "/\" D)
let D be non empty directed Subset of ; :: thesis: y "/\" (sup D) = sup ({y} "/\" D)
thus sup ({y} "/\" D) = "\/" { (y "/\" z) where z is Element of : z in D } ,S by YELLOW_4:42
.= y "/\" (sup D) by A1 ; :: thesis: verum