(t '=' u) => ((t '=' v) '=' (u '=' v)) in LD-specific-axioms by Def11;
hence (t '=' u) => ((t '=' v) '=' (u '=' v)) is LD-axiomatic by XBOOLE_0:def 3; :: thesis: verum