let IT be non empty reflexive RelStr ; :: thesis: ( IT is trivial implies IT is satisfying_MC )
assume IT is trivial ; :: thesis: IT is satisfying_MC
then reconsider I = IT as non empty trivial reflexive RelStr ;
let x be Element of IT; :: according to WAYBEL_2:def 6 :: thesis: for D being non empty directed Subset of IT holds x "/\" (sup D) = sup ({x} "/\" D)
let D be non empty directed Subset of IT; :: thesis: x "/\" (sup D) = sup ({x} "/\" D)
ex a being Element of I st the carrier of I = {a} by TEX_1:def 1;
hence x "/\" (sup D) = sup ({x} "/\" D) by STRUCT_0:def 10; :: thesis: verum