let E be set ; for s, t being Element of E ^omega holds not s ==>. t, {} ((E ^omega),(E ^omega))
let s, t be Element of E ^omega ; not s ==>. t, {} ((E ^omega),(E ^omega))
assume
s ==>. t, {} ((E ^omega),(E ^omega))
; contradiction
then consider v, w, s1, t1 being Element of E ^omega such that
s = (v ^ s1) ^ w
and
t = (v ^ t1) ^ w
and
A1:
s1 -->. t1, {} ((E ^omega),(E ^omega))
;
[s1,t1] in {} ((E ^omega),(E ^omega))
by A1;
hence
contradiction
by PARTIT_2:def 1; verum