let t be GRZ-formula; :: thesis: ( LD-EqClassOf t is LD-provable implies t is LD-provable )
set x = LD-EqClassOf t;
assume LD-EqClassOf t is LD-provable ; :: thesis: t is LD-provable
then consider u being GRZ-formula such that
A1: LD-EqClassOf u = LD-EqClassOf t and
A2: u is LD-provable ;
u LD-= t by A1, Th80;
then u '=' t is LD-provable ;
hence t is LD-provable by A2, Th61; :: thesis: verum