let x, y be LD-EqClass; :: thesis: ( x '=' y is LD-provable iff x = y )
consider t, u being GRZ-formula such that
A2: ( x = LD-EqClassOf t & y = LD-EqClassOf u ) and
A3: x '=' y = LD-EqClassOf (t '=' u) by Def93;
thus ( x '=' y is LD-provable implies x = y ) :: thesis: ( x = y implies x '=' y is LD-provable )
proof
assume x '=' y is LD-provable ; :: thesis: x = y
then t '=' u is LD-provable by A3, Th90;
hence x = y by A2, Th80, Def76; :: thesis: verum
end;
assume x = y ; :: thesis: x '=' y is LD-provable
then t '=' u is LD-provable by A2, Th80, Def76;
hence x '=' y is LD-provable by A3; :: thesis: verum