let I be 1 -element reflexive RelStr ; :: thesis: I is satisfying_MC
let x be Element of I; :: according to WAYBEL_2:def 6 :: thesis: for D being non empty directed Subset of I holds x "/\" (sup D) = sup ({x} "/\" D)
let D be non empty directed Subset of I; :: thesis: x "/\" (sup D) = sup ({x} "/\" D)
thus x "/\" (sup D) = sup ({x} "/\" D) by STRUCT_0:def 10; :: thesis: verum