theorem :: WAYBEL_4:58

for L being complete LATTICE
for AR being Relation of L st ( for x being Element of L st ex y being Element of L st y is_maximal_wrt AR -below x,AR holds
[x,x] in AR ) holds
AR is satisfying_SI