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
[s,t] in S by A2, Def4;
hence s -->. t,T by A1, Def4; :: thesis: verum