let R be Ring; :: thesis: for a, b being Element of R holds
( a | R = b | R iff a = b )
let a, b be Element of R; :: thesis: ( a | R = b | R iff a = b )

now :: thesis: ( a | R = b | R implies a = b )

assume a | R = b | R ; :: thesis: a = b
hence a = (b | R) . 0 by Th28
.= b by Th28 ;
:: thesis: verum

end;

hence ( a | R = b | R iff a = b ) ; :: thesis: verum