let L be non empty join-associative \/-SemiLattStr ; :: thesis: for a, b, c being Element of L st a [= b & b [= c holds
a [= c
let a, b, c be Element of L; :: thesis: ( a [= b & b [= c implies a [= c )
assume ( a "\/" b = b & b "\/" c = c ) ; :: according to LATTICES:def 3 :: thesis: a [= c
hence a "\/" c = c by Def5; :: according to LATTICES:def 3 :: thesis: verum