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