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

for s, t, u being Element of E ^omega st s -->. t,S holds

( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S )

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

( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S )

let s, t, u be Element of E ^omega ; :: thesis: ( s -->. t,S implies ( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S ) )

assume s -->. t,S ; :: thesis: ( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S )

then s ==>. t,S by Th10;

hence ( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S ) by Th12; :: thesis: verum

for s, t, u being Element of E ^omega st s -->. t,S holds

( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S )

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

( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S )

let s, t, u be Element of E ^omega ; :: thesis: ( s -->. t,S implies ( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S ) )

assume s -->. t,S ; :: thesis: ( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S )

then s ==>. t,S by Th10;

hence ( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S ) by Th12; :: thesis: verum