let E be set ; for s, t being Element of E ^omega st s ==>* t, {} ((E ^omega),(E ^omega)) holds
s = t
let s, t be Element of E ^omega ; ( s ==>* t, {} ((E ^omega),(E ^omega)) implies s = t )
assume
s ==>* t, {} ((E ^omega),(E ^omega))
; s = t
then
==>.-relation ({} ((E ^omega),(E ^omega))) reduces s,t
;
then
{} ((E ^omega),(E ^omega)) reduces s,t
by Th29;
then
{} reduces s,t
by PARTIT_2:def 1;
hence
s = t
by REWRITE1:13; verum