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

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