let E be set ; :: thesis: for S, T being semi-Thue-system of E
for s, t being Element of E ^omega st S c= T & s ==>* t,S holds
s ==>* t,T
let S, T be semi-Thue-system of E; :: thesis: for s, t being Element of E ^omega st S c= T & s ==>* t,S holds
s ==>* t,T
let s, t be Element of E ^omega ; :: thesis: ( S c= T & s ==>* t,S implies s ==>* t,T )
assume that
A1: S c= T and
A2: s ==>* t,S ; :: thesis: s ==>* t,T
==>.-relation S reduces s,t by A2, Def7;
then ==>.-relation T reduces s,t by A1, Th26, REWRITE1:23;
hence s ==>* t,T by Def7; :: thesis: verum