theorem Th97: :: GRZLOG_1:41
for t, u being GRZ-formula holds LD-EqClassOf (t => u) = (LD-EqClassOf t) => (LD-EqClassOf u)