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 A1: GRZ-axioms , GRZ-rules |- t ;
GRZ-axioms c= LD-axioms by XBOOLE_1:7;
then LD-axioms , GRZ-rules |- t by A1, Th44;
hence t is LD-provable ; :: thesis: verum