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