let E be set ; :: thesis: for S, T being semi-Thue-system of E st S c= T holds
==>.-relation S c= ==>.-relation T
let S, T be semi-Thue-system of E; :: thesis: ( S c= T implies ==>.-relation S c= ==>.-relation T )
assume A1: S c= T ; :: thesis: ==>.-relation S c= ==>.-relation T
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ==>.-relation S or x in ==>.-relation T )
assume A2: x in ==>.-relation S ; :: thesis: x in ==>.-relation T
then consider s, t being object such that
A3: x = [s,t] and
A4: ( s in E ^omega & t in E ^omega ) by RELSET_1:2;
reconsider s = s, t = t as Element of E ^omega by A4;
s ==>. t,S by A2, A3, Def6;
then s ==>. t,T by A1, Th19;
hence x in ==>.-relation T by A3, Def6; :: thesis: verum