let t be GRZ-formula; :: thesis: ( t is GRZ-provable implies t is LD-provable )
assume t is GRZ-provable ; :: thesis: t is LD-provable
then GRZ-axioms , GRZ-rules |- t ;
then LD-axioms , GRZ-rules |- t by Th44;
hence t is LD-provable ; :: thesis: verum