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