let t, u be GRZ-formula; :: thesis: LD-EqClassOf (t => u) = (LD-EqClassOf t) => (LD-EqClassOf u)
thus LD-EqClassOf (t => u) = (LD-EqClassOf t) '=' (LD-EqClassOf (t '&' u)) by Def93
.= (LD-EqClassOf t) => (LD-EqClassOf u) by Def92 ; :: thesis: verum