for L being non empty join-associative \/-SemiLattStr
for a, b, c being Element of L st a [= b & b [= c holds
a [= c by Def5;