let E be set ; :: thesis: for s, t being Element of E ^omega holds not s ==>. t, {} ((E ^omega),(E ^omega))
let s, t be Element of E ^omega ; :: thesis: not s ==>. t, {} ((E ^omega),(E ^omega))
assume s ==>. t, {} ((E ^omega),(E ^omega)) ; :: thesis: 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; :: thesis: verum