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