theorem Th96: :: GRZLOG_1:40
for t, u being GRZ-formula holds LD-EqClassOf (t 'or' u) = (LD-EqClassOf t) 'or' (LD-EqClassOf u)