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
thus for x being set st x in ==>.-relation S holds
x in ==>.-relation T :: according to TARSKI:def 3 :: thesis: verum

proof

let x be set ; :: thesis: ( x in ==>.-relation S implies x in ==>.-relation T )
assume A2: x in ==>.-relation S ; :: thesis: x in ==>.-relation T
then consider s, t being set such that
A3: x = [s,t] and
A4: ( s in E ^omega & t in E ^omega ) by RELSET_1:6;
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

end;