for S being non empty reflexive RelStr st ( 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) ) holds
S is satisfying_MC