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)
consider a being Element of I such that
A1: the carrier of I = {a} by TEX_1:def 1;
thus x "/\" (sup D) = sup ({x} "/\" D) by A1, STRUCT_0:def 10; :: thesis: verum