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 ) by Def5;
[s1,t1] in {} (E ^omega ),(E ^omega ) by A1, Def4;
hence contradiction by OPOSET_1:def 1; :: thesis: verum