let x, y be LD-EqClass; :: thesis: ( ( x => y is LD-provable & y => x is LD-provable ) iff x = y )
thus ( x => y is LD-provable & y => x is LD-provable implies x = y ) :: thesis: ( x = y implies ( x => y is LD-provable & y => x is LD-provable ) )

proof

assume that
A1: x => y is LD-provable and
A2: y => x is LD-provable ; :: thesis: x = y
thus x = x '&' y by A1, Th92
.= y by A2, Th92 ; :: thesis: verum

end;

assume x = y ; :: thesis: ( x => y is LD-provable & y => x is LD-provable )
hence ( x => y is LD-provable & y => x is LD-provable ) by Th92; :: thesis: verum