:: deftheorem defines satisfying_SI WAYBEL_4:def 20 :
for L being RelStr
for AR being Relation of L holds
( AR is satisfying_SI iff for x, z being Element of L st [x,z] in AR & x <> z holds
ex y being Element of L st
( [x,y] in AR & [y,z] in AR & x <> y ) );