let E be set ; :: thesis: for S, T being semi-Thue-system of E

for s, t being Element of E ^omega holds

( not s ==>. t,S \/ T or s ==>. t,S or s ==>. t,T )

let S, T be semi-Thue-system of E; :: thesis: for s, t being Element of E ^omega holds

( not s ==>. t,S \/ T or s ==>. t,S or s ==>. t,T )

let s, t be Element of E ^omega ; :: thesis: ( not s ==>. t,S \/ T or s ==>. t,S or s ==>. t,T )

assume s ==>. t,S \/ T ; :: thesis: ( s ==>. t,S or s ==>. t,T )

then consider v, w, s1, t1 being Element of E ^omega such that

A1: ( s = (v ^ s1) ^ w & t = (v ^ t1) ^ w ) and

A2: s1 -->. t1,S \/ T ;

A3: [s1,t1] in S \/ T by A2;

for s, t being Element of E ^omega holds

( not s ==>. t,S \/ T or s ==>. t,S or s ==>. t,T )

let S, T be semi-Thue-system of E; :: thesis: for s, t being Element of E ^omega holds

( not s ==>. t,S \/ T or s ==>. t,S or s ==>. t,T )

let s, t be Element of E ^omega ; :: thesis: ( not s ==>. t,S \/ T or s ==>. t,S or s ==>. t,T )

assume s ==>. t,S \/ T ; :: thesis: ( s ==>. t,S or s ==>. t,T )

then consider v, w, s1, t1 being Element of E ^omega such that

A1: ( s = (v ^ s1) ^ w & t = (v ^ t1) ^ w ) and

A2: s1 -->. t1,S \/ T ;

A3: [s1,t1] in S \/ T by A2;